Abstract
We introduce a general purpose typed λ-calculus λ∞ which contains intuitionistic logic, is capable of internalizing its own derivations as λ-terms and yet enjoys strong normalization with respect to a natural reduction system. In particular, λ∞ subsumes the typed λ-calculus. The Curry-Howard isomorphism converting intuitionistic proofs into λ∞terms is a simple instance of the internalization property of λ∞. The standard semantics of λ∞ is given by a proof system with proof checking capacities. The system λ∞ is a theoretical prototype of reflective extensions of a broad class of type-based systems in programming languages, provers, AI and knowledge representation, etc.
The research described in this paper was supported in part by ARO under the MURI program “Integrated Approach to Intelligent Systems”, grant DAAH04-96-1-0341, by DARPA under program LPE, project 34145.
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
S. Artemov, “Operational Modal Logic,” Tech. Rep. MSI 95-29, Cornell University, December 1995 http://www.cs.cornell.edu/Info/People/artemov/MSI95-29.ps
S. Artemov, “Uniform provability realization of intuitionistic logic, modality and lambda-terms”, Electronic Notes on Theoretical Computer Science, vol. 23, No. 1. 1999 http://www.elsevier.nl/entcs
S. Artemov, “Explicit provability and constructive semantics”, The Bulletin for Symbolic Logic, v.7, No. 1, pp. 1–36, 2001 http://www.cs.cornell.edu/Info/People/artemov/BSL.ps.
H. Barendregt, “Lambda calculi with types”. In Handbook of Logic in Computer Science, vol.2, Abramsky, Gabbay, and Maibaum, eds., Oxford University Press, pp. 118–309, 1992
R. Constable, “Types in logic, mathematics and programming”. In Handbook in Proof Theory, S. Buss, ed., Elsevier, pp. 683–786, 1998
D. de Jongh and G. Japaridze, “Logic of Provability”, in S. Buss, ed., Handbook of Proof Theory, Elsevier, pp. 475–546, 1998
.J.-Y. Girard, Y. Lafont, P. Taylor, Proofs and Types, Cambridge University Press, 1989.
V.N. Krupski, “Operational Logic of Proofs with Functionality Condition on Proof Predicate”, Lecture Notes in Computer Science, v. 1234, Logical Foundations of Computer Science’ 97, Yaroslavl’, pp. 167–177, 1997
V.N. Krupski, “The single-conclusion proof logic and inference rules specification”, Annals of Pure and Applied Logic, v.110, No. 1-3, 2001 (to appear).
A. Nerode, “Applied Logic”. In The merging of Disciplines: New Directions in Pure, Applied, and Computational Mathematics, R.E. Ewing, K.I. Gross, C.F. Martin, eds., Springer-Verlag, pp. 127–164, 1986
A. Troelstra, “Realizability”. In Handbook in Proof Theory, S. Buss, ed., Elsevier, pp. 407–474, 1998
A.S. Troelstra and H. Schwichtenberg, Basic Proof Theory, Cambridge University Press, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alt, J., Artemov, S. (2001). Reflective λ-Calculus. In: Kahle, R., Schroeder-Heister, P., Stärk, R. (eds) Proof Theory in Computer Science. PTCS 2001. Lecture Notes in Computer Science, vol 2183. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45504-3_2
Download citation
DOI: https://doi.org/10.1007/3-540-45504-3_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42752-0
Online ISBN: 978-3-540-45504-2
eBook Packages: Springer Book Archive