The intensional lambda calculus

Título:

The intensional lambda calculus

Autor:

Artemov, Sergei

Colaboradores:

; Bonelli, Eduardo

Temas:

CÁLCULO LAMBDALENGUAJES FORMALESLENGUAJES DE PROGRAMACIÓN

En:

Logical Foundations of Computer Science. Berlín : Springer, 2007. (Lecture Notes in Computer Science; 4514), pp. 12-25

Resumen:

We introduce a natural deduction formulation for the Logic of Proofs, a refinement of modal logic S4 in which the assertion PA 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.

URL/DOI:

http://dx.doi.org/10.1007/978-3-540-72734-7_2

Medio:

Soporte electrónico

Tipo de documento:

Artículo

Descripción física:

1 archivo (285,8 KB)

Idioma:

Inglés

Publicación:

Springer, 2007

Puede solicitar más fácilmente el ejemplar con: A0275

Ver estantes