Alfa is a successor of the proof editor ALF, i.e., an editor for direct manipulation of proof objects in a logical framework based on Per Martin-Löf's Type Theory. 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.
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. In fact, the language is very similar to the functional language Cayenne by Lennart Augustsson.
Alfa is being developed by people in
The Programming Logic
Group at Chalmers. Alfa uses a
proof checker
developed initially by Thierry Coquand (V3)
and developed further by Catarina Coquand
(Agda).
The most recent development of Agda has been made by
Makoto Takeyama. He has added the new
idata construction, to regain some of the power available through
the inductive data definitions found in the old ALF system.
Alfa also has some support for working with natural language translations of proofs, by interfacing to Aarne Ranta's Grammatical Framework, GF.
The graphical user interface and the infrastructure that glues everything together is implemented by Thomas Hallgren. It is all written in Haskell.
Alfa is available on the Unix computers at
the department. It can be started with the command
alfa.
External users can download Alfa, see below.
Alfa is known to work on the following platforms (October 2000):