Introduction to ALF - a Background

Catarina Coquand

In 6th NWPT, page 157

Abstract:

We will give an introduction to type theory, focussing on its use as a logical framework for proofs and programs. We will also discuss the use of inductive definition as specifications and proofs by pattern matching. Many examples will be presented.
The basic idea behind using type theory for developing proofs and programs is the Curry-Howard isomorphism between propositions and types. Take for example the proposition ( implies implies ). Looking at this proposition as a type we see that this is the type of the combinator. In type theory we then say that the combinator proofs the proposition ( implies implies ).

The language that is used is a functional language with dependent types. Hence programs and proofs can be described in the same language. We use inductive definitions for our specifications. Introduction rules in logic corresponds to defining a type by its constructors. Proofs are functions defined by pattern matching over these types. We shall also mention how this can be extended to proofs about infinite objects.

Comments
Chalmers Technical University, Inst. for Computer Science, Göteborg, Sweden. E-mail: catarina@cs.chalmers.se.

Available as PostScript, DVI.

BRICS WWW home page