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.

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Malgorzata Biernacka, Olivier Danvy, Kristian Støvring
• Keywords: Applicative-order Reduction, ENTCS 2006, First-order Minimal Logic, Weak Head Normalization