TY - GEN
T1 - The intensional lambda calculus
AU - Artemov, Sergei
AU - Bonelli, Eduardo
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=35448996871&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=35448996871&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-72734-7_2
DO - 10.1007/978-3-540-72734-7_2
M3 - Conference contribution
AN - SCOPUS:35448996871
SN - 3540727329
SN - 9783540727323
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 12
EP - 25
BT - Logical Foundations of Computer Science - International Symposium, LFCS 2007, Proceedings
T2 - International Symposium on Logical Foundations of Computer Science, LFCS 2007
Y2 - 4 June 2007 through 7 June 2007
ER -