View on GitHub

Andromeda

Your type theory à la Martin-Löf

ICFP 2019 material

Introduction

Information about the old Andromeda 1, an implementation of type theory with equality reflection, is available here.

Andromeda 2 is currently under active development. Until better documentation will be available, the best way to learn about Andromeda 2 is by consulting the code examples found in theories subdirectory and the tests subdirectory.

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.

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.