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.

If you want to 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):

Update 2017-08-26: some updates to make the code compile with the current version of GHC has been made. A source snapshot (a Cabal package) and a binary installer package for macOS are available.
26 Aug 2017 20:47 Thomas Hallgren