33 Alfa -- a proof editor for type theory

Alfa is a WYSIWYG proof editor. It allows you to, interactively and incrementally, define theories (axioms and inference rules), formulate theorems and construct proofs of the theorems. All steps in the proof construction are immediately checked by the system and no erroneous proofs can be constructed. The logical framework used is one of Thierry Coquand's versions of Per Martin-Löf's Type Theory.

Alternatively, you can view Alfa as a syntax-directed editor for a small purely functional programming language with a type system that provides dependent types. The editor immediately checks that programs you enter are syntactically correct and type correct.

Alfa is largely inspired by Window-Alf [AGNvS94], implemented by Lena Magnusson and Johan Nordlander, and has a similar user interface.

The plan is that Alfa should improve on Window-Alf by

Some of this has been implemented. As shown in Figure 90, proofs can be presented in natural deduction style.

Figure 90. Window dump of Alfa, illustrating the construction of a simple proof in natural deduction style.

Whereas Window-Alf was implemented in Standard ML (proof engine) and C++ & Interviews (user interface), Alfa is implemented entirely in Haskell, using Fudgets for the user interface. At the time of writing, the source code consists of about 8000 lines, distributed as follows:

In addition, Aarne Ranta has supplied 2100 lines with support for natural language. Some of this code had been integrated in Alfa, but this work was in a rather experimental stage.

More detailed and up-to-date information on Alfa is available on the WWW [Hal97].