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
Research projects
- Type Theory for Data-Intensive Formalization (TyDiForm), principal investigator, Air Force Office of Scientific Research
- Computationally intensive methods, member, Slovenian Research Agency
Publications
Research papers:
- papers at math.andrej.com
- papers at arXiv.org
Research talks:
- talks at math.andrej.com
- video recordings of talks on YouTube
Bibliography:
- official bibliography at COBISS
- DBLP
- Google scholar
- MathSciNet (may require authentication)
- ORCID 0000-0001-5378-0547
Blog:
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.
Software
- Coop
- A prototype programming language for programming with runners, also known as comodels.
- Andromeda
- Andromeda is an implementation of dependent type theory with equality reflection. The type theory is very expressive, as it allows one to postulate new judgmental equalities.
- Eff
- Eff is a functional language with handlers, a generalization of the usual exception handlers through which we can manipulate state, I/O, and other computational effects. The handlers can also be used to implement transactions, redirection, backtracking, multi-threading, and many other programming concepts.
- Programming Languages Zoo
- The Programming Languages Zoo is a collection of miniature programming languages which demonstrates various concepts and techniques used in programming language design and implementation. It is a good starting point for those who would like to implement their own programming language, or just learn how it is done.
- Marshall
- Marshall is a programming language for exact real arithmetic based on ideas from Abstract Stone Duality.
- Alg
- Alg is a program for enumeration of finite models of single-sorted first-order theories. These include groups, rings, fields, lattices, posets, graphs, and many more.
- RZ
- RZ is a tool for automatic generation of program specifications from mathematical theories. The purpose of RZ is to help programmers and mathematicians design data structures which properly implement mathematical structures (algebras, real numbers, Hilbert spaces, etc.)
- Analytica
- An automated theorem prover implemented in Mathematica.
- repositories and gists
- other projects at GitHub