Introduction to ALF - a Background

# 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