Program Extraction from Normalization Proofs
Ulrich Berger, Stefan Berghofer, Pierre Letouzey, Helmut Schwichtenberg · Studia Logica · 2006
This paper describes formalizations of Tait's normalization proof for the simply typed λ-calculus in the proof assistants Minlog, Coq and Isabelle/HOL. From the formal proofs programs are machine-extracted that implement variants of the well-known normalization-by-evaluation algorithm. The case study is used to test and compare the program extraction machineries of the three proof assistants in a non-trivial setting.