Philipp Georg Haselwarter: Andromeda 2.0
Source: Mathematics and theoretical computing seminar
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.