*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.

- 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 mouse buttons. (Not written yet.)
- Overview of the keyboard.
- Printing Alfa documents.
- Using Alfa plug-in modules.

**Tutorials**:- Getting started with Alfa. (Not written yet.)
**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 6 July 2009).
- Known Bugs (updated on 6 July 2009).
- My TODO list. (Local access only)

- 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.

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)

Thomas Hallgren