@article{Biernacka_Danvy_Støvring_2005, title={Program Extraction from Proofs of Weak Head Normalization}, volume={12}, url={https://tidsskrift.dk/brics/article/view/21878}, DOI={10.7146/brics.v12i12.21878}, abstractNote={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.}, number={12}, journal={BRICS Report Series}, author={Biernacka, Malgorzata and Danvy, Olivier and Støvring, Kristian}, year={2005}, month={Apr.} }