Vallauris

Égide funds integrated actions (PAI - "les programmes d'actions intégrées") between France and Spain via the Programme Picasso. Beginning January 2005, this program is funding a scientific proposal with the title

Integrating Proof Theoretic techniques and Semantic Tools in Proof Carrying Code and Validation and Analysis of Declarative code

This integrated action is between INRIA-Futurs, coordinated by Dale Miller, and the Universidad Politècnica de Madrid, coordinated by James Lipton. We will use the name Vallauris for this project: it is also the name of a small town in the south of France where Picasso lived and worked for a couple of years after World War II.

Personnel

From the INRIA-Futurs side, the two teams of Parsifal and Comète are currently involved.

From the Universidad Politècnica de Madrid side, the two groups are also involved.

Departamento de Inteligencia Artificial. In particular, Manuel Hermenegildo, Francisco Bueno, German Puebla, Daniel Cabeza, Manuel Carro, Pedro Lopez Garcia.
WIthin the Departamento de Inteligencia Artificial Departamento de Lenguajes y Sistemas Informáticos e Ingeniería del Software, there are the groups of Laboratorio de Metodologías y Lenguajes and Unidad de Programación. In particular, Juan José Moreno Navarro, Julio Mariño Carballo, Susana Muñoz Hernández, and Angel Herranz.

Project Summary

The two research groups involved in this proposal have approached the problem of analysis of declarative code using different but complementary techniques. The Paris group at the Ecole Polytechnique has applied structural proof theory to define higher-order and linear extensions to declarative code that permit a logical, declarative approach to the formalization of modules, proof-carrying code, and the syntax of object programming languages for subsequent implementation and analysis.

The Madrid group has developed type-free higher-order extensions and a module system, on top of which it has built a preprocessor capable of carrying out static analysis of the module structure as well as the underlying language. The techniques are semantics-based, using abstract interpretation and operational semantics sensitive to computational properties of the code. All of these components are integrated into the Ciao multi-paradigm programming platform. Cooperation of these groups would provide opportunities for interaction of these two communities that is almost without precedent in the area of multi-paradigm integration, as there has been an unnecessary divide between semantics-based and proof-theory based techniques.

News

05-07.12.2005

Jim Lipton visits LIX for discussions and to give a talk.

28-30 November 2005

Miller travels to Madrid to discuss project topics.

5 October 2005

Many members of this team attends the MoveLog 2005 workshop at ICLP in order to kick-off this collaboration.

5 June 2006

The LIX PhD student, Olivier Hermant, travelled to Madrid to work with Jim Lipton.

Keywords

Proof Carrying Code, Higher Order Logic Programming, Logic Programming, Abstract Interpretation, Declarative programming, Linear logic.

Last modified 15.10.06.