Lógica de pruebas para certificación de computación móvil

En este trabajo se presenta un modelo para computaciones móviles que incluye la generación de certificados al estilo PCC (proof carrying code). El modelo consiste en un lenguaje de programación recortado, un sistema de tipos y una semántica basada en una máquina abstracta. El cálculo es obtenido a p...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autor principal:	Feller, Federico
Otros Autores:	Bonelli, Eduardo
Formato:	Tesis Tesis de grado
Lenguaje:	Español
Publicado:	2009
Materias:	Ciencias Informáticas lenguaje de programación lógica matemática y lenguajes formales Programación Informática
Acceso en línea:	http://sedici.unlp.edu.ar/handle/10915/3958
Aporte de:	SEDICI (UNLP) de Universidad Nacional de La Plata

id	I19-R120-10915-3958
record_format	dspace
institution	Universidad Nacional de La Plata
institution_str	I-19
repository_str	R-120
collection	SEDICI (UNLP)
language	Español
topic	Ciencias Informáticas lenguaje de programación lógica matemática y lenguajes formales Programación Informática
spellingShingle	Ciencias Informáticas lenguaje de programación lógica matemática y lenguajes formales Programación Informática Feller, Federico Lógica de pruebas para certificación de computación móvil
topic_facet	Ciencias Informáticas lenguaje de programación lógica matemática y lenguajes formales Programación Informática
description	En este trabajo se presenta un modelo para computaciones móviles que incluye la generación de certificados al estilo PCC (proof carrying code). El modelo consiste en un lenguaje de programación recortado, un sistema de tipos y una semántica basada en una máquina abstracta. El cálculo es obtenido a partir de una técnica inspirada en el isomorfismo de Curry-DeBruijn-Howard, en donde las proposiciones y pruebas de una lógica son interpretadas como los tipos y términos de un lenguaje. En este caso la lógica elegida es ILPnd, una representación en deducción natural de la versión intuicionista de la lógica de pruebas LP. Estas lógicas son lógicas modales con la característica especial que contienen el operador modal de la forma [s]A, que se interpreta como “s es una prueba A”. La interpretación computacional de este operador es el de código móvil que computa un valor de tipo A con certificado s. A esta combinación de código y certificado se la denomina unidad móvil. A partir de la definición formal del cálculo se estudian un conjunto de propiedades sobre el mismo que incluyen seguridad de tipos y normalización fuerte. Adicionalmente, se presenta una implementación del cálculo en un lenguaje funcional.
author2	Bonelli, Eduardo
author_facet	Bonelli, Eduardo Feller, Federico
format	Tesis Tesis de grado
author	Feller, Federico
author_sort	Feller, Federico
title	Lógica de pruebas para certificación de computación móvil
title_short	Lógica de pruebas para certificación de computación móvil
title_full	Lógica de pruebas para certificación de computación móvil
title_fullStr	Lógica de pruebas para certificación de computación móvil
title_full_unstemmed	Lógica de pruebas para certificación de computación móvil
title_sort	lógica de pruebas para certificación de computación móvil
publishDate	2009
url	http://sedici.unlp.edu.ar/handle/10915/3958
work_keys_str_mv	AT fellerfederico logicadepruebasparacertificaciondecomputacionmovil
bdutipo_str	Repositorios
_version_	1764820472761942018

Lógica de pruebas para certificación de computación móvil

Ejemplares similares