Normal view MARC view ISBD view

The intensional lambda calculus

By:

Artemov, Sergei

Contributor(s):

Bonelli, Eduardo

Material type: Article

ArticleDescription: 1 archivo (285,8 KB)Subject(s):

Online resources:

Click here to access online

Summary: 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.

Average rating: 0.0 (0 votes)

Holdings ( 1 )
Title notes ( 3 )

Holdings
Item type	Home library	Collection	Call number	URL	Status	Date due	Barcode
Capítulo de libro	Biblioteca de la Facultad de Informática	Biblioteca digital	A0275 (Browse shelf(Opens below))	Link to resource	No corresponde

Browsing Biblioteca de la Facultad de Informática shelves, Collection: Biblioteca digital Close shelf browser (Hides shelf browser)

Previous								Next
Previous	A0272 Deriving requirements specifications from the application domain language captured by Language Extended Lexicon	A0273 Formal concept analysis-based service classification to dynamically build efficient software component directories	A0274 Generating a catalog of unanticipated schemas in class hierarchies using formal concept analysis	A0275 The intensional lambda calculus	A0276 Developing DSLs using combinators : a design pattern	A0277 Services conceptualization within SOA/BPM methodology	A0278 A fine grained aspect coordination mechanism	Next

Formato de archivo: PDF. -- Este documento es producción intelectual de la Facultad de Informática - UNLP (Colección BIPA/Biblioteca)

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.

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