Sciweavers

Share
ENTCS
2006

Program Extraction From Proofs of Weak Head Normalization

3 years 8 months ago
Program Extraction From Proofs of Weak Head Normalization
We formalize two proofs of weak head normalization for the simply typed lambdacalculus 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. Key words: program extraction, normalization by evaluation, weak head normalization.
Malgorzata Biernacka, Olivier Danvy, Kristian St&o
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Malgorzata Biernacka, Olivier Danvy, Kristian Støvring
Comments (0)
books