**
Program extraction from normalization proofs
**

*
Ulrich Berger
*

**Abstract**

From a constructive proof of strong normalization
plus uniqueness of the long beta-normal form for the
simply typed lambda-calculus a normalization program is extracted
using Kreisel`s modified realizability interpretation for intuitionistic
logic. The proof - which uses Tait's computability predicates -
is not completely formalized: Induction is done on the meta level,
and therefore not a single program but a family
of program, one for each term is obtained. Nevertheless
this may be used to write a short and efficient normalization
program in a type free programming functional programming
language (e.g. LISP) which has the interesting feature that it first
evaluates a term r of type rho to a functional |r| of type
rho and then collapses |r| to the normal form of r.

**Bib entry**

InProceedings{Berger93a, author = "Ulrich Berger", title = "Program extraction from normalization proofs", editor = "M. Bezem and J.F. Groote", volume = "664", series = "LNCS", pages = "91--106", booktitle = "Typed Lambda Calculi and Applications", year = "1993", publisher = "Springer-Verlag"}