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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
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)