zbMATH — the first resource for mathematics

The intensional lambda calculus. (English) Zbl 1132.03318
Artemov, Sergei N. (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2007, New York, NY, USA, June 4–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72732-3/pbk). Lecture Notes in Computer Science 4514, 12-25 (2007).
Summary: We introduce a natural deduction formulation for the Logic of Proofs, a refinement of modal logic S4 in which the assertion \(\square 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 \(\lambda ^{I}\) that internalises intensional information on how a term is computed. In the same way that the Logic of Proofs internalises its own derivations, \(\lambda ^{I}\) internalises its own computations. Confluence and strong normalisation of \(\lambda ^{I}\) is proved. This system serves as the basis for the study of type theories that internalise intensional aspects of computation.
For the entire collection see [Zbl 1121.03005].

03B40 Combinatory logic and lambda calculus
03B45 Modal logic (including the logic of norms)
03B70 Logic in computer science
Full Text: DOI