The logic of proofs as a foundation for certifying mobile computation (Record no. 55718)
[ view plain ]
000 -CABECERA | |
---|---|
campo de control de longitud fija | 01720naa 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 | 20250311170417.0 |
008 - DATOS DE LONGITUD FIJA--INFORMACIÓN GENERAL | |
campo de control de longitud fija | 230201s2009 xx o 000 0 eng d |
024 8# - Otro identificador estandar | |
Número estándar o código | DIF-M6516 |
-- | 6655 |
-- | DIF005936 |
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 | Bonelli, Eduardo |
245 10 - MENCIÓN DE TÍTULO | |
Título | The logic of proofs as a foundation for certifying mobile computation |
300 ## - DESCRIPCIÓN FÍSICA | |
Extensión | 1 archivo (293,4 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 explore an intuitionistic fragment of Artemov's Logic of Proofs as a type system for a programming language for mobile units. Such units consist of both a code and certificate component. Dubbed the Certifying Mobile Calculus, our language caters for both code and certificate development in a unified theory. In the same way that mobile code is constructed out of code components and extant type systems track local resource usage to ensure the mobile nature of these components, our system additionally ensures correct certificate construction out of certificate components. We present proofs of type safety and strong normalistion for a run-time system based on an abstract machine. |
534 ## - NOTA SOBRE LA VERSIÓN ORIGINAL | |
Encabezamiento principal del original | Logical Foundations of Computer Science : International Symposium, LFCS 2009, Deerfield Beach, FL, USA, January 3-6, 2009. Proceedings. Berlín : Springer, 2009. (Lecture Notes in Computer Science ; 5407), pp. 76-91 |
650 #4 - PUNTO DE ACCESO ADICIONAL DE MATERIA--TÉRMINO DE MATERIA | |
Término de materia o nombre geográfico como elemento de entrada | COMPUTACIÓN MÓVIL |
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 |
650 #4 - PUNTO DE ACCESO ADICIONAL DE MATERIA--TÉRMINO DE MATERIA | |
Término de materia o nombre geográfico como elemento de entrada | PROGRAMACIÓN LÓGICA |
700 1# - PUNTO DE ACCESO ADICIONAL--NOMBRE DE PERSONA | |
Nombre de persona | Feller, Federico |
856 40 - LOCALIZACIÓN Y ACCESO ELECTRÓNICOS | |
Identificador Uniforme del Recurso | <a href="http://dx.doi.org/10.1007/978-3-540-92687-0_6">http://dx.doi.org/10.1007/978-3-540-92687-0_6</a> |
942 ## - ELEMENTOS DE PUNTO DE ACCESO ADICIONAL (KOHA) | |
Tipo de ítem Koha | Capítulo de libro |
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 | A0283 | 11/03/2025 | http://catalogo.info.unlp.edu.ar/meran/getDocument.pl?id=542 | 11/03/2025 | Capítulo de libro |