My research is motivated by the desire to understand the connection between mathematics and computation. My areas of interest are
- foundations of mathematics and logic
- constructive and computable mathematics
- homotopy type theory
- mathematical foundations of programming languages
- exact scientific computation
Curriculum vitae ยท ORCID 0000-0001-5378-0547
Research projects
- Bridging AI, Proof Assistants, and Mathematical Data (BRIDGE), principal investigator, Renaissance Philanthropy
- Type Theory for Data-Intensive Formalization (TyDiForm), principal investigator, Air Force Office of Scientific Research
- Computationally intensive methods, member, Slovenian Research Agency
Publications
See the Publications page for a complete bibliography a list of selected papers.
Talks
See the Talks page for a list of selected lectures and talks.
Software
- Andromeda
- A proof assistant with user-definable type theories.
- Eff
- A functional language with algebraic effects and handlers.
- Programming Languages Zoo
- A collection of miniature programming languages for learning PL design and implementation.
- Marshall
- A programming language for exact real arithmetic based on Dedekind reals.
- Coop
- A prototype programming language for programming with runners (comodels).
- Alg
- A program for enumeration of finite models of single-sorted first-order theories.
- RZ
- A tool for automatic generation of program specifications from mathematical theories.
- Analytica
- An automated theorem prover implemented in Mathematica.
- repositories and gists
- Other projects on GitHub.
Formalized mathematics
- HoTT library
- The HoTT library is a development of homotopy type theory in the Coq proof assistant.
- General type theories
- Formalization of general type theories in the Coq proof assistant.