next up previous
Next: A first example Up: A user's guide to Previous: Contents


ALF ("Another logical framework") is a structure editor for Martin-Löf's monomorphic type theory; i.e. it ensures that the constructed objects are wellformed and welltyped. It can be used for the development of proofs and programs and for the integrated verification of functional programs. ALF emphasizes the interactive development of type-theoretic constructions, i.e. proof objects and programs, using a window-based user interface. Thus ALF supports an arbitrary mixture of top-down and bottom-up development.

A logical framework is a pure dependent Type Theory. It is an open theory, i.e. the user can add constants and equations. In the current implementation of ALF there is no check whether the theory is consistent. However, the user can restrict herself to the set theory described in e.g. Nordström, Petersson, Smith: Programming in Martin-Löf's Type Theory (Oxford University Press 1990) - this is implemented as a library. New inductive sets can be added, e.g. following the schemas in Dybjer's Inductive Families. ALF also supports Coquand's discipline of Pattern Matching in Type Theory . For more background information on the type theory used in ALF, look at Type theory and Programming.

The basic metaphor of ALF is the refinement of an incomplete proof object which is displayed in a window (scratch area). By using the mouse the user can fill in placeholders by first pointing to them and then selecting a previously constructed object from a menu. ALF uses unification to fill in further placeholders automatically. If this is not yet possible, ALF generates a set of constraints, which can also be manipulated from the user interface. Once the construction of the current object has been completed, the object is moved to another more permanent window (theory window).

ALF has been used to formalize parts of intuitionistic mathematics and to verify simple programs. Examples include

Björn von Sydow
Thu May 17 13:05:14 MET 1996