|
Program Extraction from Proofs of Weak Head Normalization
Magorzata Biernacka
April 2005 |
Abstract:
We formalize two proofs of weak head normalization for the
simply typed lambda-calculus in first-order minimal logic: one for
normal-order reduction, and one for applicative-order reduction in the object
language. Subsequently we use Kreisel's modified realizability to extract
evaluation algorithms from the proofs, following Berger; the proofs are based
on Tait-style reducibility predicates, and hence the extracted algorithms are
instances of (weak head) normalization by evaluation, as already identified
by Coquand and Dybjer
Available as PostScript, PDF, DVI. |