MARC details
| 000 -LEADER |
|---|
| campo de control de longitud fija |
01689naa a2200277 a 4500 |
| 003 - IDENTIFICADOR DE NÚMERO DE CONTROL |
|---|
| campo de control |
AR-LpUFIB |
| 005 - FECHA Y HORA DE LA ÚLTIMA TRANSACCIÓN |
|---|
| campo de control |
20240131183025.0 |
| 007 - CAMPO FIJO DE DESCRIPCIÓN FÍSICA--INFORMACIÓN GENERAL |
|---|
| campo de control de longitud fija |
ta |
| 008 - DATOS DE LONGITUD FIJA--INFORMACIÓN GENERAL |
|---|
| campo de control de longitud fija |
230201s2007 xx do 000 0 eng d |
| 024 8# - IDENTIFICADOR DE OTROS ESTÁNDARES |
|---|
| Número estándar o código |
DIF002996 |
| 040 ## - FUENTE DE CATALOGACIÓN |
|---|
| Centro catalogador/agencia de origen |
AR-LpUFIB |
| Lengua de catalogación |
spa |
| Centro/agencia transcriptor |
AR-LpUFIB |
| 100 1# - ENTRADA PRINCIPAL--NOMBRE DE PERSONA |
|---|
| Nombre de persona |
Artemov, Sergei |
| 9 (RLIN) |
254586 |
| 245 10 - MENCIÓN DEL TÍTULO |
|---|
| Título |
The intensional lambda calculus |
| 260 ## - PUBLICACIÓN, DISTRIBUCIÓN, ETC. |
|---|
| Lugar de publicación, distribución, etc. |
ref_localidad@NULL : |
| Nombre del editor, distribuidor, etc. |
Springer, |
| Fecha de publicación, distribución, etc. |
2007 |
| 300 ## - DESCRIPCIÓN FÍSICA |
|---|
| Extensión |
1 archivo (285,8 KB) |
| 500 ## - NOTA GENERAL |
|---|
| Nota general |
Formato de archivo: PDF. -- Este documento es producción intelectual de la Facultad de Informática - UNLP (Colección BIPA/Biblioteca) |
| 520 ## - RESUMEN, ETC. |
|---|
| Sumario, etc. |
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. |
| 534 ## - NOTA SOBRE LA VERSIÓN ORIGINAL |
|---|
| Encabezamiento principal del original |
Logical Foundations of Computer Science. Berlín : Springer, 2007. (Lecture Notes in Computer Science; 4514), pp. 12-25 |
| 650 #4 - PUNTO DE ACCESO ADICIONAL DE MATERIA--TÉRMINO DE MATERIA |
|---|
| Término de materia o nombre geográfico como elemento de entrada |
CÁLCULO LAMBDA |
| 9 (RLIN) |
253468 |
| 650 #4 - PUNTO DE ACCESO ADICIONAL DE MATERIA--TÉRMINO DE MATERIA |
|---|
| Término de materia o nombre geográfico como elemento de entrada |
LENGUAJES FORMALES |
| 9 (RLIN) |
247830 |
| 650 #4 - PUNTO DE ACCESO ADICIONAL DE MATERIA--TÉRMINO DE MATERIA |
|---|
| Término de materia o nombre geográfico como elemento de entrada |
LENGUAJES DE PROGRAMACIÓN |
| 9 (RLIN) |
43382 |
| 700 1# - ENTRADA AGREGADA--NOMBRE PERSONAL |
|---|
| Nombre de persona |
Bonelli, Eduardo |
| 9 (RLIN) |
251743 |
| 856 40 - LOCALIZACIÓN Y ACCESO ELECTRÓNICOS |
|---|
| Identificador Uniforme de Recursos |
<a href="http://dx.doi.org/10.1007/978-3-540-72734-7_2">http://dx.doi.org/10.1007/978-3-540-72734-7_2</a> |
| 856 40 - LOCALIZACIÓN Y ACCESO ELECTRÓNICOS |
|---|
| Identificador Uniforme de Recursos |
<a href=" http://catalogo.info.unlp.edu.ar/meran/getDocument.pl?id=536"> http://catalogo.info.unlp.edu.ar/meran/getDocument.pl?id=536</a> |
| 942 ## - ELEMENTOS DE ENTRADA SECUNDARIOS (KOHA) |
|---|
| Tipo de ítem Koha |
Capítulo de libro |