The project members participate in the development and curation of the following freely available software, formalization libraries, and databases of mathematical structures.
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ć.
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.
A formalization of general type theories and fundamental meta-theorems about them, developed by Peter LeFanu Lumsdaine, Andrej Bauer, and Philipp Haselwarter.
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.
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.
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č.
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.
A list of databases of mathematical structures, curated by Katja Berčič.
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.