Sciweavers

ENTCS
2006

Program Extraction From Proofs of Weak Head Normalization

13 years 11 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)