The project members participate in the development and curation of the following freely available software, formalization libraries, and databases of mathematical structures.

Type theory and formalized mathematics


Andromeda is an experimental proof assistant that support user-definable type theories, designed in the tradition of LCF proof assistants. It is currently maintained by Andrej Bauer, Philipp Haselwater, and Anja Petković.

HoTT library

The HoTT library is a formalization of homotopy type theory in the Coq proof assistant. It is one of the largest and oldest formalizations of its kind. It was initiated by Andrej Bauer, and is currently maintained by an international team of researchers.


Egbert Rijke formalized a large proportion of his upcoming textbook on homotopy type theory in the Agda proof assistant. The library contains several different areas of mathematics, ranging from foundations of type theory and discrete mathematics, to synthetic homotopy theory.

General type theories

A formalization of general type theories and fundamental meta-theorems about them, developed by Peter LeFanu Lumsdaine, Andrej Bauer, and Philipp Haselwarter.

Programming languages


Eff is the first programming language with first-class algebraic effect and handlers, created by Andrej Bauer and Matija Pretnar. It has inspired the development of similar languages and incorporation of algebraic effects and handlers into other languages and libraries. It was originally created by Andrej Bauer and Matija Pretnar.


Æff is an experimental programming language for programming with asynchronous algebraic effects. It was created by Danel Ahman and Matija Pretnar.


Coop is a prototype programming language for programming with runners, also known as comodels. It supports modular and extensible management of computational resources, with strong guarantee of proper finalization. It was created by Danel Ahman and Andrej Bauer.


Millet is an experimental pure ML-like language with simple and modular codebase, intended as a template for experimentation and implementation with new programming language features. It was created by Matija Pretnar.

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.

Databases of mathematical structures


MathDataHub provides dataset hosting and a searchable interface for databases of mathematical structures. It is part of MathHub, a portal for active mathematical documents and an archive for flexiformal mathematics. The database is maintained by the KWARZ research group from the University Friedrich-Alexander University in Erlangen-Nürenberg, in cooperation with Katja Berčič.

Discrete Zoo

A central repository of discrete objects with a website front-end and extensions for mathematical software packages, maintained by Katja Berčič and Janoš Vidali.

Catalogoue of Mathematical Datasets

A list of databases of mathematical structures, curated by Katja Berčič.

Miscellaneous resources


Marshall is a programming language for exact real arithmetic based on ideas from Abstract Stone Duality. It was developed by Andrej Bauer and Paul Taylor.


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. It was developed by Andrej Bauer and Aleš Bizjak.