| 000 | 01512naa a2200241 a 4500 | ||
|---|---|---|---|
| 003 | AR-LpUFIB | ||
| 005 | 20250311170302.0 | ||
| 008 | 230201s2007 xx o 000 0 eng d | ||
| 024 | 8 |
_aDIF-M6509 _b6647 _zDIF003007 |
|
| 040 |
_aAR-LpUFIB _bspa _cAR-LpUFIB |
||
| 100 | 1 | _aArtemov, Sergei | |
| 245 | 1 | 0 | _aThe intensional lambda calculus |
| 300 | _a1 archivo (285,8 KB) | ||
| 500 | _aFormato de archivo: PDF. -- Este documento es producción intelectual de la Facultad de Informática - UNLP (Colección BIPA/Biblioteca) | ||
| 520 | _aWe 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. | ||
| 534 | _aLogical Foundations of Computer Science. Berlín : Springer, 2007. (Lecture Notes in Computer Science; 4514), pp. 12-25 | ||
| 650 | 4 | _aCÁLCULO LAMBDA | |
| 650 | 4 | _aLENGUAJES FORMALES | |
| 650 | 4 | _aLENGUAJES DE PROGRAMACIÓN | |
| 700 | 1 | _aBonelli, Eduardo | |
| 856 | 4 | 0 | _uhttp://dx.doi.org/10.1007/978-3-540-72734-7_2 |
| 942 | _cCP | ||
| 999 |
_c52862 _d52862 |
||