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.

If you want to download Alfa, see below.

Alfa Documentation

• Features of Alfa. Brief description of Alfa and its implementation. Plans for future improvements. Limitations of the current version.
• Alfa User's Guide.
• Quick reference pages:
  • Command line syntax and options.
  • Top 10 ways to fill in a place holder.
  • Overview of the menus.
  • Overview of the keyboard.
  • Printing Alfa documents.
  • Using Alfa plug-in modules.
• Tutorials:
  • Editing by using the keyboard only.
  • Constructing proofs in Natural Deduction style.
  • Using the GF plug-in to produce natural language translations of proofs.
• Alfa Library/Example Modules.

• History of changes. News about Alfa (updated on ).
• Known Bugs (updated on ).

Links

• Agda. The proof engine used in Alfa.
• GF - the Grammatical Framework, which is used in Alfa to translate proofs to and from natural language.
• Other Proof Assistants in the dmoz open directory.

Download Alfa

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

• NetBSD 1.4/i386, FreeBSD 3.2/i386, Redhat Linux/i386 (version 5.2, 6.2 and 7.0)
• SunOS-5.x/sparc (=Solaris 2.x)

Update 2020-10-26: updated source packages for Fudgets and Alfa are now available, to make it easier to compile Alfa with recent versions of GHC. The binary installer package for macOS mentioned above is still available as well.