Abstract
We show how to extract classical programs expressed in Krivine λ c -calculus from proof-terms built in a proof-irrelevant and classical version of the calculus of constructions with universes. For that, we extend Krivine’s realisability model of classical second-order arithmetic to the calculus of constructions with universes using a structure of Π-set which is reminiscent of ω-sets, and show that our realisability model validates Peirce’s law and proof-irrelevance. Finally, we extend the extraction scheme to a primitive data-type of natural numbers in a way which preserves the whole compatibility with the classical realisability interpretation of second-order arithmetic.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aczel, P.: On relating type theories and set theories. In: Altenkirch, Naraschewski, Reus (eds.) Proceedings of Types 1998 (1999)
Altenkirch, T.: Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh (November 1993)
Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 120(76), 95 (1988)
Geuvers, J.H., Nederhof, M.J.: A modular proof of strong normalization for the calculus of constructions. Journal of Functional Programming 1,2(1991), 155–189 (1991)
Hyland, J.M.E.: The effective topos. In: Troelstra, A.S., van Dalen, D. (eds.) The L. E. J. Brouwer Centenary Symposium, North Holland, Amsterdam (1982)
Krivine, J.-L.: Lambda-calcul, types et modèles. Masson (1991)
Krivine, J.-L.: A general storage theorem for integers in call-by-name lambda-calculus. Th. Comp. Sc. 129, 79–94 (1994)
Krivine, J.-L.: Typed lambda-calculus in classical Zermelo-Fraenkel set theory. Arch. Math. Log. 40(3), 189–205 (2001)
Krivine, J.-L.: Dependent choice, ‘quote’ and the clock. Th. Comp. Sc. 308, 259–276 (2003)
Krivine, J.-L.: Realizability in classical logic. Unpublished lecture notes (available on the author’s web page) (2005)
Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 200–219. Springer, Heidelberg (2003)
Longo, G., Moggi, E.: A category-theoretic characterization of functional completeness. Theor. Comput. Sci. 70(2), 193–211 (1990)
Luo, Z.: Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, Oxford (1994)
Melliès, P.-A., Werner, B.: A generic normalisation proof for pure type systems. In: Giménez, E., Paulin-Mohring, C. (eds.) TYPES 1996. LNCS, vol. 1512, pp. 254–276. Springer, Heidelberg (1998)
Miquel, A.: Le calcul des constructions implicite: syntaxe et sémantique. PhD thesis, Université Paris 7 (2001)
Paulin-Mohring, C.: Extracting Fω’s programs from proofs in the calculus of constructions. In: POPL 1989, pp. 89–104 (1989)
Paulin-Mohring, C.: Définitions Inductives en Théorie des Types d’Ordre Supérieur. Habilitation à diriger les recherches, Université Claude Bernard Lyon I (1996)
The Coq Development Team (LogiCal Project). The Coq Proof Assistant Reference Manual - Version 8.1. Technical report, INRIA (2006)
Streicher, T.: Semantics of Type Theory. Birkhäuser (1991)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Miquel, A. (2007). Classical Program Extraction in the Calculus of Constructions. In: Duparc, J., Henzinger, T.A. (eds) Computer Science Logic. CSL 2007. Lecture Notes in Computer Science, vol 4646. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74915-8_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-74915-8_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74914-1
Online ISBN: 978-3-540-74915-8
eBook Packages: Computer ScienceComputer Science (R0)