Subproyecto 4: Universidad Complutense de Madrid

    Investigador Principal: Ricardo Peña Departamento de Sistemas Informáticos y Programación, Facultad de Informática, Universidad Complutense de Madrid ricardo@sip.ucm.es
Módulo M-4.1: Diseño del lenguaje de alto nivel y del compilador-certificador.
    El objetivo de este módulo es crear un lenguaje funcional con suficientes restricciones de forma que los programas con él construidos puedan certificarse fácilmente como correctos con respecto a ciertas políticas de seguridad. Incluye el diseño del sistema de tipos y efectos con el que se analiza la corrección de los programas y la construcción del compilador-certificador para dicho lenguaje.

Módulo M-4.2: Diseño de la máquina abstracta imperativa y del comprobador de certificados.

    El objetivo de este módulo es diseñar una máquina abstracta y un código máquina (bytecode) cercanos a Java que sirva como plataforma destino para el compilador certificador desarrollado en el módulo M.4.1. El diseño incluye dotar a las instrucciones máquina de un sistema de tipos anotados que permitan expresar el consumo de memoria (montón y pila) por parte de los programas. Dicho sistema de tipos ha de ser correcto con respecto a la semántica de las instrucciones máquina. El intérprete de dicha máquina recibirá programas anotados con sus tipos y comprobará que ambos, programa y tipos, son consistentes.