Open AccessProgram Extraction from Proofs of Weak Head Normalization
Author(s) -
Małgorzata Biernacka,
Olivier Danvy,
Kristian Støvring
Publication year - 2005
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v12i12.21878
Subject(s) - mathematical proof , realizability , normalization (sociology) , computer science , calculus (dental) , programming language , mathematics , lambda calculus , discrete mathematics , algorithm , theoretical computer science , algebra over a field , pure mathematics , geometry , medicine , dentistry , sociology , anthropology
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.