Program Extraction from Proofs of Weak Head Normalization
AbstractWe 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.
How to Cite
Biernacka, M., Danvy, O., & Støvring, K. (2005). Program Extraction from Proofs of Weak Head Normalization. BRICS Report Series, 12(12). https://doi.org/10.7146/brics.v12i12.21878
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.