The intensional lambda calculus

Sergei Artemov, Eduardo Bonelli

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

15 Scopus citations

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.

Original languageEnglish
Title of host publicationLogical Foundations of Computer Science - International Symposium, LFCS 2007, Proceedings
Pages12-25
Number of pages14
DOIs
StatePublished - 2007
EventInternational Symposium on Logical Foundations of Computer Science, LFCS 2007 - New York, NY, United States
Duration: 4 Jun 20077 Jun 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4514 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Symposium on Logical Foundations of Computer Science, LFCS 2007
Country/TerritoryUnited States
CityNew York, NY
Period4/06/077/06/07

Fingerprint

Dive into the research topics of 'The intensional lambda calculus'. Together they form a unique fingerprint.

Cite this