|
|||||
|
|
Program Extraction from Normalization Proofs |
|
| Authors: | Ulrich Berger Stefan Berghofer Pierre Letouzey Helmut Schwichtenberg |
| Affiliation: | 1. Department of Computer Science, University of Wales Swansea, Singleton Park, Swansea, SA2 8PP, UK 2. Institut für Informatik, Technische Universit?t München, Boltzmannstr. 3, D-85748, Garching, Germany 3. Laboratoire P.P.S., Université Denis Diderot, Case 7014, 2 Place Jussieu, F-75251, Paris, Cedex 05, France 4. Mathematisches Institut der Universit?t München, Theresienstr. 39, D-80333, München, Germany |
| Abstract: | 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. |
| Keywords: | Normalization by evaluation typed lambda calculus realizability program extraction from proofs |
| 本文献已被 SpringerLink 等数据库收录！ | |