View on GitHub

Andromeda

Type theory with equality reflection

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.

The design of Andromeda follows the tradition of LCF-style theorem provers:

The nucleus does not perform any normalization (it cannot as the underlying type theory has no normal forms), unification, or perform proof search. These techniques can all be implemented on top of the nucleus in AML, and therefore cannot compute underivable judgments by design. Of course, they could fail or run forever because AML is a general-purpose programming language.

Equality checking is delegated to the meta-level by a mechanism of operations and handlers akin to those of the Eff programming language. Whenever the nucleus needs to check a non-trivial equation, it triggers an operation (question) which propagates to the meta-level. There it is intercepted by a user-defined handler which handles (answers) the equation by providing a witness for it.

Theoretical background

Documents: see the documents folder in the GitHub repository.

History of the name

Andromeda used to be called Brazil, as a consequence of discussions at the Institute for Advanced Study where we talked about “sending proofs to a far away place where they will check them independently”. We thought of Brazil as a faraway place, but it later turned out it was not quite far enough. Martin Escardó suggested the name Andromeda. We hope that nobody will claim that our neighboring galaxy is a nearby place.

Developers

Travis Continuous Integration

The GitHub repository is linked to Travis CI. The current build status:

Build Status

Support

This material is based upon work supported by the Air Force Office of Scientific Research, Air Force Materiel Command, USAF under Award No. FA9550-14-1-0096. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the author(s) and do not necessarily reflect the views of the Air Force Office of Scientific Research, Air Force Materiel Command, USAF.