Alfa (particle traces)

[P svenska]

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-Lf'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 Documentation


Download Alfa

(The binary distributions are not available any more, due to reorganization. Thank you, Chalmers.)

Alfa is known to work on the following platforms (October 2000):

5 Jul 2012 19:45 Thomas Hallgren