Mathematics and Computation

A blog about mathematics for computers

Software contributions by Andrej Bauer

Andromeda : a proof assistant with user-definable type theories

HoTT library : a formalization of homotopy type theory in the Coq proof assistant

Eff : a functional language with algebraic effects and handlers

Programming Languages Zoo : a collection of miniature programming languages

Marshall : a programming language for exact real arithmetic based on Dedekind reals

RZ : a tool for automatic generation of specifications based on realizability theory

Alg : a program that generates finite models of a first-order theory

For a complete list, visit my GitHub repositories.