INVESTIGADORES
BONELLI Eduardo Augusto
artículos
Título:
The Intensional Lambda Calculus
Autor/es:
SERGEI ARTEMOV, EDUARDO BONELLI
Revista:
LECTURE NOTES IN COMPUTER SCIENCE
Editorial:
Springer-Verlag
Referencias:
Año: 2007 vol. 4514 p. 12 - 25
ISSN:
0302-9743
Resumen:
We introduce a natural deduction formulation for the Logic of Proofs, a refinement of modal logic S4 in which the assertion Box 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.
