Abstract
We introduce a natural deduction formulation for the Logic of Proofs, a refinement of modal logic S4 in which the assertion □ A is replaced by [[s]]A whose intended reading is “s is a proof of A”. A term calculus for this formulation yields a typed lambda calculus λ I that internalises intensional information on how a term is computed. In the same way that the Logic of Proofs internalises its own derivations, λ I internalises its own computations. Confluence and strong normalisation of λ I is proved. This system serves as the basis for the study of type theories that internalise intensional aspects of computation.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alt, J., Artemov, S.N.: Reflective λ-calculus. In: Kahle, R., Schroeder-Heister, P., Stärk, R.F. (eds.) PTCS 2001. LNCS, vol. 2183, p. 22. Springer, Heidelberg (2001)
Artemov, S., Bonelli, E.: The intensional lambda calculus. Technical report (December 2006), http://www.lifia.info.unlp.edu.ar/~eduardo/lamIFull.pdf
Artemov, S.: Operational modal logic. Technical Report MSI 95-29, Cornell University (1995)
Artemov, S.: Proof realization of intuitionistic and modal logics. Technical Report MSI 96-06, Cornell University (1996)
Artemov, S.: Unified semantics of modality and λ-terms via proof polynomials. In: Algebras, Diagrams and Decisions in Language, Logic and Computation, pp. 89–118 (2001)
Barendregt, H.P.: Lambda Calculi with Types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 2, Oxford University Press, Oxford (1992)
Brezhnev, V.: On the logic of proofs. In: Striegnitz, K. (ed.) Proceedings of the Sixth ESSLLI Student Session, pp. 35–45 (2001)
Church, A., Rosser, J.B.: Some properties of conversion. Transactions of the American Mathematical Society 39, 472–482 (1936)
Davies, R., Pfenning, F.: A modal analysis of staged computation. In: Steele Jr., G. (ed.) Proceedings of the 23rd Annual Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, January 1996, pp. 258–270. ACM Press, New York (1996)
Davies, R., Pfenning, F.: A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science 11, 511–540 (2001)
Davies, R., Pfenning, F.: A modal analysis of staged computation. Journal of the ACM 48(3), 555–604 (2001)
Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1989)
Huet, G., Lévy, J.-J.: Computations in orthogonal rewriting systems. In: Lassez, J.L., Plotkin, G.D. (eds.) Computational Logic; Essays in honor of Alan Robinson, pp. 394–443. MIT Press, Cambridge (1991)
Klop, J.W.: Combinatory Reduction Systems. PhD thesis, CWI, Amsterdam, Mathematical Centre Tracts no.127 (1980)
Khasidashvili, Z., Ogawa, M., van Oostrom, V.: Perpetuality and uniform normalization in orthogonal rewrite systems. Information and Computation 164, 118–151 (2001)
Lévy, J.-J.: Réductions correctes et optimales dans le lambda-calcul. PhD thesis, Université Paris VII (1978)
Martin-Löf, P.: On the meaning of the logical constants and the justifications of the logical laws. Lectures given at the meeting Teoria della Dimostrazione e Filosofia della Logica, in Siena, 6-9 April 1983, by the Scuola di Specializzazione in Logica Matematica of the Università degli Studi di Siena (1983)
Nipkow, T.: Higher-order critical pairs. In: Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, July 1991, IEEE Computer Society Press, Los Alamitos (1991)
TERESE: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (March 2003)
Wickline, P., Lee, P., Pfenning, F., Davies, R.: Modal types as staging specifications for run-time code generation. ACM Computing Surveys 30(3es) (1998)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Artemov, S., Bonelli, E. (2007). The Intensional Lambda Calculus. In: Artemov, S.N., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2007. Lecture Notes in Computer Science, vol 4514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72734-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-72734-7_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72732-3
Online ISBN: 978-3-540-72734-7
eBook Packages: Computer ScienceComputer Science (R0)