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

Draft copy

Errata