The intensional lambda calculus (Record no. 52862)

MARC details
000 -CABECERA
campo de control de longitud fija 01512naa a2200241 a 4500
003 - IDENTIFICADOR DEL NÚMERO DE CONTROL
campo de control AR-LpUFIB
005 - FECHA Y HORA DE LA ÚLTIMA TRANSACCIÓN
campo de control 20250311170302.0
008 - DATOS DE LONGITUD FIJA--INFORMACIÓN GENERAL
campo de control de longitud fija 230201s2007 xx o 000 0 eng d
024 8# - Otro identificador estandar
Número estándar o código DIF-M6509
-- 6647
-- DIF003007
040 ## - FUENTE DE LA 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
245 10 - MENCIÓN DE TÍTULO
Título The intensional lambda calculus
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 ## - SUMARIO, 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
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
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
700 1# - PUNTO DE ACCESO ADICIONAL--NOMBRE DE PERSONA
Nombre de persona Bonelli, Eduardo
856 40 - LOCALIZACIÓN Y ACCESO ELECTRÓNICOS
Identificador Uniforme del Recurso <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>
942 ## - ELEMENTOS DE PUNTO DE ACCESO ADICIONAL (KOHA)
Tipo de ítem Koha Capítulo de libro
Holdings
Estado de retiro Estado de pérdida Estado dañado Disponibilidad Colección Biblioteca permanente Biblioteca actual Fecha de adquisición Total de préstamos Signatura topográfica completa Fecha visto por última vez Identificador Uniforme del Recurso Precio válido a partir de Tipo de ítem Koha
      No corresponde Biblioteca digital Biblioteca de la Facultad de Informática Biblioteca de la Facultad de Informática 11/03/2025   A0275 11/03/2025 http://catalogo.info.unlp.edu.ar/meran/getDocument.pl?id=536 11/03/2025 Capítulo de libro