Program Extraction from Normalization Proofs

, , &
Studia Logica 82 (1):25-49 (2006)
  Copy   BIBTEX

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.

Categories

Keywords

Reprint years

DOI

10.1007/s11225-006-6604-5

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,053

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Alexander Leitsch/From the Editor 3–5 Matthias Baaz and Rosalie Iemhoff/Gentzen Calculi for the Existence Predicate 7–23 Ulrich Berger, Stefan Berghofer, Pierre Letouzey and Helmut Schwichtenberg/Program Extraction from. [REVIEW]Alexander Leitsch - 2006 - Studia Logica 82:40.
A Mixed λ-calculus.Marie-Renée Fleury & Myriam Quatrini - 2007 - Studia Logica 87 (2-3):269-294.
A formalization of Sambins's normalization for GL.Edward Hermann Haeusler & Luiz Carlos Pereira - 1993 - Mathematical Logic Quarterly 39 (1):133-142.
Programs from proofs using classical dependent choice.Monika Seisenberger - 2008 - Annals of Pure and Applied Logic 153 (1-3):97-110.
A Formalization Of Sambins's Normalization For Gl.Edward Hauesler & Luiz Carlos Pereira - 1993 - Mathematical Logic Quarterly 39 (1):133-142.
Ontological Proofs of Existence and Non-Existence.Petr Hájek - 2008 - Studia Logica 90 (2):257-262.
Strong normalization in type systems: A model theoretical approach.Jan Terlouw - 1995 - Annals of Pure and Applied Logic 73 (1):53-78.
Variants of Gödel’s Ontological Proof in a Natural Deduction Calculus.B. Woltzenlogel Paleo & Annika Kanckos - 2017 - Studia Logica 105 (3):553-586.
Term-Space Semantics of Typed Lambda Calculus.Ryo Kashima, Naosuke Matsuda & Takao Yuyama - 2020 - Notre Dame Journal of Formal Logic 61 (4):591-600.
Natural deduction for non-classical logics.David Basin, Seán Matthews & Luca Viganò - 1998 - Studia Logica 60 (1):119-160.

Analytics

Added to PP
2009-01-28

Downloads
86 (#236,836)

6 months
9 (#423,873)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Towards the computational complexity of ℘Rω-terms.Karl-Heinz Niggl - 1995 - Annals of Pure and Applied Logic 75 (1):153-178.

Add more citations

References found in this work

Interpretation of analysis by means of constructive functionals of finite types.Georg Kreisel - 1959 - In A. Heyting (ed.), Constructivity in mathematics. Amsterdam,: North-Holland Pub. Co.. pp. 101--128.

Add more references