** Next:** A first example
**Up:** A user's guide to
** Previous:** Contents

## Introduction

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

- a proof that Ackermann's function is not primitive recursive.
- the fundamental theorem of arithmetic.
- functional completeness of combinatory logic.
- Higman's lemma and an intuitionistic version of Ramsey's theorem.
- a normalization proof for intuitionistic propositional logic.
- formalization of pointfree topology with applications.
- derivation of various simple functional programs.
- formalization of notions from process calculus.
- a proof of correctness of graph reduction.

*Björn von Sydow *

Thu May 17 13:05:14 MET 1996