Sciweavers

76
Voted
TLCA
1993
Springer
15 years 26 days 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