Philipp Georg Haselwarter: Andromeda 2.0

Abstract: In joint work with Peter LeFanu Lumsdaine and Andrej Bauer we have developed a notion of `General Type Theories' (GTT), with the intention of giving a mathematically precise description of a class of dependent type theories in the style of Martin-Löf, and studying their meta-theory. For example, intensional type theory with universes and homotopy type theory form instances of GTTs.

In current ongoing work with Andrej Bauer we implemented the GTT framework in what will be the second major version of the Andromeda proof assistant: Andromeda 2.0.

In this talk I will give an introduction to General Type Theories, and outline the architecture of Andromeda. I will explain the representation of type theory in Andromeda, and discuss how it relates to the meta-theoretical properties we have proven for GTTs. To finish, there will be a little demonstration of the system in action.