Andrej Bauer

My research is motivated by the desire to understand the connection between mathematics and computation. My areas of interest are

Research projects


Research papers:

Research talks:



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.


A prototype programming language for programming with runners, also known as comodels.
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 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 is a programming language for exact real arithmetic based on ideas from Abstract Stone Duality.
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 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.)
An automated theorem prover implemented in Mathematica.
repositories and gists
other projects at GitHub