Philipp Georg Haselwarter: Andromeda 2.0
Vir: Seminar za temelje matematike in teoretično računalništvo
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.