Author: Stefan Berghofer
Title: Extracting a normalization algorithm from a proof of weak normalization for the simply-typed Lambda-calculus
Abstract:
Typed $\lambda$-calculi play an important role in computer science,
both as a foundation for functional programming languages and for
theorem provers. A particularly important result for typed
$\lambda$-calculi is the normalization theorem, stating that each
well-typed term can be reduced to a normal form. We describe the
formalization of a proof of the weak normalization theorem for
simply-typed $\lambda$-calculus based on de Bruijn indices in the
theorem prover Isabelle/HOL. This proof is entirely contructive,
and therefore contains an algorithm computing the normal form
of a $\lambda$-term. We show how this algorithm, together with
a proof of its correctness, can automatically be extracted
from this proof within Isabelle/HOL.