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"}