Program Extraction from Normalization Proofs

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.

• Type: Conference
• Year: 1993
• Where: TLCA
• Authors: Ulrich Berger
• Keywords: Formal Proofs Programs, Proof Assistants, Tait’s Normalization Proof, Theoretical Computer Science, TLCA 1993