Implementation of Proof Editors

Our group has a long experience in the development of languages and systems for interactive development of proofs and programs, one of the first was ALF . The language that was implemented was based on Martin-Löf's Framework.

The latest version is Agda. The language it is implementing is Structured Type Theory which is a dependently typed functional language with modern language constructs such as parametrised modules and records. It is quite close to Cayenne. The user can interact with Agda through an emacs-interface, or a graphical interface, Alfa.

We also have a simple web-based proof editor for propositional logic Alfie, which is intended for use in elementary teaching.