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

Abstract

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.