Controllo e certificazione dell'uso delle risorse

:: Home

:: Kickoff meeting

:: Final meeting

:: Project Description

CONCERTO (CONtrol and CERTification of Resources Usage) is a Project di Rilevanza Nazionale (PRIN), funded by the Italian Ministero dell'Istruzione, dell'Università e della Ricerca (MIUR). It lasts 24 months, from September 2008 to August 2010.

CONCERTO is the ideal continuation of MIUR-2004 FOLLIA project (Logical foundations of abstract programming languages) and of MIUR-2002 PROTOCOLLO project (from PROofs TO COmputation through Linear LOgic).

The kickoff meeting of CONCERTO had take place in Bologna, from February 16 to February 18, 2009.

The final meeting of CONCERTO (joint meeting with the Projet CNRS PICS 'Logique Linéaire et applications') will take place in Torino, from June 09 to June 11, 2010.

Partners of CONCERTO are:

Abstract of the project

The project focuses on formal foundations for language-based (especially static) techniques guaranteeing resource-related runtime properties of programs, both in the sequential and in the concurrent computational model. Such static resource management is of increasing importance in the domain of embedded, mobile, and distributed computing. The project belongs to the research area whose aim is to associate to a program a certification assuring some computational properties, and in particular the quantification of resources (time, space, etc.) necessary to its execution.

We will derive the tools and techniques for our investigation from the field of logical proof-theory and semantics, with special interest on linear logic and lambda-calculus.

We will work on two main objectives:

1. Foundational techniques for the analysis and verification of runtime properties of programs;

2. Computational theories modeling the correct interaction with the environment.

As for (1), we will be mainly interested in studying formal systems expressing programs of limited complexity (running time or used space), as opposed to similar systems which merely characterize functions of limited complexity. Starting from the so-called "light" logics, we will develop type systems with these characteristics, expressing a wide range of programs. We plan to experiment with certain parallel implementation techniques for optimal lambda reduction (PELCR), incorporating resource control. The objective, however, calls also for a new, deep understanding of the semantics of sequential computation. Under this respect we will study stability for a paradigmatic calculus (PCF), and we plan to study the construction of semantical models for PCF and related calculi.

As for (2), existing computational models, and especially new, emerging ones (e.g., quantum or biological computation), still need formal semantic models of their interaction with resources. Here we cannot promise implementations or tools. We plan instead to have unifying, semantical theories helping in future formal development. We plan, in particular, to study the semantics of Implicit Computational Complexity, with the aim of unifying different systems and have common ground for their comparison or extension. We will use semantical tools derived from linear logic, such as the notion of experiment, context semantics, and geometry of interaction. To develop new logical tools we also need a foundational investigation. We plan to investigate the connections between Linear Logic, in particular proof-nets, and concurrent and parallel computation model. Correctness for MALL proof-nets which are stable under fully local cut reduction steps are an important step in this direction. Finally, we plan to apply these foundational tools to the quantum and biological computational models. We will design a quantum lambda-calculus, a type system for it, and we will study the relations of these with complexity classes. We will explore the possibility of representing biological networks by a stochastic version of the differential net semantics (another linear logic tool).

In summary, we plan to develop formal tools, and to attack foundational problems at the border of logic (both proof-theory and semantics), language design, and computational complexity, with the aim to provide sound grounds for the design and development of resource-bounded certified programs.