IsoOsi.gif
ProToCoLLo
from proof to computation through linear logic
Meetings and Workshops
Organization Documents
 Publications

News:

Corso di Avviamento Alla Ricerca 

by Jean-Yves GIRARD


Description


"ProToCoLLo" is a research project partially funded by the Ministero dell'Istruzione, Università e Ricerca (MIUR) .

Project number : 2002018192.

Scientific Coordinator :  Simona Ronchi Della Rocca  -  Dipartimento di Informatica, Università di Torino


Principal Partners and Contacts:


Duration : 24 months (2003-2004).


KEYWORD:  linear logic; proof-nets ; ludics ; light linear logic ; game semantics ; elementary linear logic ; coherence spaces.

Summary of Project


The aim of this project is to further develop promising research arguments both foundational and applicative, all arising from Linear Logic (LL), inside the field of Theoretical Computer Science. Indeed it is a common opinion that logic is one of the most important theoretical tools in Computer Science, and LL opened new lines in this direction, some partially explored. We learned from the definition of LL that some logical connectives, which were considered atomic, are composite. In fact the essential property of LL is the decomposition of the intuitionistic implication A=>B in !A-oB. A linear implication A-oB represents a transformation process, that, taken as input ONE object belonging to A, gives as output ONE object belonging to B. The modality ! denotes a different process, which gives explicit evidence to intensional properties of the object A to be transformed. These properties describe the potentiality of the object to be either duplicated or deleted during the transformation. So LL supports primitive operators for duplication and erasure, which are only present at a meta-level in the standard approach. Such operators can be used to control how the proofs are built and executed (i.e., normalized). Through the well known connection between logical proofs and functional languages, formalized in the so-called "Curry-Howard morphism", LL allows to define a computable function as composition of a duplication/erasure operation followed by a linear function. Another example is the modality § of the Light Linear Logic (LLL), which further decomposes the duplication operation, so allowing to control the normalization time. This new view-point allows to model programming languages with an explicit resources control, both in space and time. Moreover LL introduced a new approach to proof theory, through the notion of "proof-net". Proof-nets are proofs (programs, via Curry-Howard correspondence) characterized by pure geometrical properties (the "correctness criteria"). They are an essential tool for refining the logical system, for studying its dynamic aspects (proofs normalization) and for characterizing fragment of the system with particular computational properties (like the polarized linear logic or the low complexity systems). Particular notations for proof-nets have been studied, which allow to define normalization procedures based on local operations, making incremental duplications. An interesting application of these properties is the design of interpreters for functional languages using optimal reduction strategies. LL gave new tools for studying the semantics of computations: coherence spaces, functional domains more refined than the previous Scott domains, for studying the denotational semantics, and the "game semantics", which is a synthesis of the two classical approaches to semantics, the operational and the denotational one. Game semantics can be fruitfully used for building fully abstract models.
 Recently from LL Ludics sprouted. In a very synthetic way, Ludics can be described as a new approach to the study of logical rules, based on a revised notion of game, whose main characteristic is the physical localization of formulas/resources. It seems to open a new scenario, when the classical distinction between syntax and semantics aims to disappear. It is interesting to explore its possible applications to Computer Science. In conclusion LL turned the classical relationships between proof theory and computation theory: in this context the present research project want both to study LL in itself and to start from LL to design new tools for the development of Theoretical Computer Science, in particular in the field of Programming Languages. The project will be organized into three lines:

 1) Structural proof theory
 2) Study of computations of fixed complexity
 3) Semantics of both proofs and programming languages.

 The first line is clearly foundational. Along it we want both to study problems related to the proof theory of LL, and to export proof theory techniques from LL to other systems (for example, classical logic). Along the second line, we want in particular to study logics derived from LL, with the property of characterizing computations of given complexity, and to explore their possible applications to programming languages. Along the third line, we want to deal with semantics. In particular we want both to model the meaning of logical systems (in particular of proof-nets) and to use tools from LL (e.g. game theory or coherence spaces) for studying the formal semantics of programming languages.


Last modified: 30 January 2004