Sciweavers

TLCA
1993
Springer
13 years 9 months ago
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 p...
Ulrich Berger