Blanc SIMI 2 - Sciences de l'information, de la matière et de l'ingénierie : Sciences de l’information, simulation

Logic and Geometry of Interaction – LOGOI

Logic and Geometry of Interaction

The Logic of Interaction and the Nature of Computation

PROOFS AND PROGRAMS NEED NEW FOUNDATIONS, PLACING INTERACTION AT THE CENTER OF THE PICTURE

The project LOGOI is situated at the interface between mathematical logic and computer science. Proof-theory has a well-established role in providing theoretical bases (semantics) and mathematical tools for the study and development of programming languages. In particular, a key rôle has been played by the Curry-Howard correspondence, in which proofs in a formal system can be seen as programs, and normalization of the proofs as execution of the programs. <br />The evolution of computing is bringing in the foreground new issues such as cooperation of agents, data exchange between processes, shared resources, where interaction has a primary role; moreover, new paradigms, such as quantum computing, are developing. This evolution puts us in a completely new situation : it challenges proof theory and is forcing semantics to revisit its foundations and elaborate new concepts and methods. <br /> <br />In this setting, placing interaction at the center of the picture seems fundamental ; for this reason, the base of the LOGOI project was Geometry of Interaction, an approach to proof theory, made possible by the introduction of Linear Logic, and which had seen important advances in recent years. The core of Geometry of Interaction is a dynamical interpretation of logic and calculus. The processes (proves, via the Curry-Howard correspondence) are defined by their interactive behaviour. Thes framework is then especially well suited to the analysis of HOW the computation is performed, taking into account the procedural content of computation as well as the time of execution. Moreover, its mathematical foundation on the theory of Operator Algebras opens fascinating connections with Quantum Theory.

The assumption underlying our proposal is that proof theory and computer science can be given new mathematical foundations, and that we can seek insight from mathematical fields, such as analysis, geometry, and measure theory which have been the subject of intense development in contemporary mathematics, to such an extent that there now exist radically new ideas and insights on them. Recent developments in Geometry of Interaction had opened the way to make this possible, and were hence the basis of our project. We expected in particular to gain insights into complexity theory, which is in some sense the effective version of infinity. There are several approaches to computational complexity; however, the whole theory appears to be fundamentally lacking structure. So far complexity theory seems to be a collection of ad hoc techniques, useful for addressing a single, often deep question, while clueless in front of other questions. Virtually all of the characterizations given so far have a very strong existential content (i.e., ``a problem is in class iff there exists«) as opposed to a more appealing universal content. Another main objective of our investigation was to open the way for a theory of expressiveness for programming languages; one is interested not only in WHAT is computed, but also at HOW computation is performed. All these lines have the potential to yield interesting applications.

There have been important advances in all tasks of the project; we believe that the bases of a really new approach are emerging from these efforts.The development of the  mathematical  theory has led both to a renewal of the syntax  of proofs, and advances in the  foundation for a theory of interaction (Abstract Machines/Games). A main result of this is the foundation of a radically new approach to computational complexity, where the methodology and new tools to deal with inifinity comes from Geometry of Interaction, and its interpretation in the operator algebras. We have gained  new intuitions on expressiviness of programming languages  and  computational models. Applications involve  currently very active research fields, such as  quantum computing, concurrency,  and parallel computation.

Among the successes of LOGOI, we stress also :

* high involvement of students ; Logoi has directly involved 20 PhD students and several stages at Master level : so far, 9 PhD thesis produced within the project have been defended.

* dissemination and visibility: 2 schools and several workshops

* the establishment of a rich net of international collaborations

There have been important advances in all the tasks of the project; we believe that the bases of a really new approach are emerging from these efforts. Moreover, with Logoi we have built around our approach a strong and well connected group of researchers, and established a network of international collaborations, which we want to continue in the future.

Publications (reviewed ): 44 , of which 25% multi-partners

International Journals: 15
Proceedings of International Conferences: 28
Proceedings of French Conferences: 1

PhD Thesis : 9

The project LOGOI is situated at the interface between mathematical logic and computer science.
Proof-theory has a well-established role in providing theoretical bases (semantics) and mathematical tools for the study and development of programming languages.
The evolution of computing is bringing in the foreground new issues such as cooperation of agents, data exchange between processes, shared resources, where interaction has a primary role; moreover, new paradigms, such as quantum computing, are developing. This evolution puts us in a completely new situation. It challenges proof theory and is forcing semantics to revisit its foundations and elaborate new concepts and methods.
Geometry of Interaction has a great potential as a framework in which to develop such a program.

The project of Geometry of Interaction, which started together with Linear Logic, is that of a dynamical interpretation of logic and calculus; it alllows the unification, within a powerful setting, the two programming paradigms based on proof-theory: the paradigm of proofs-as-programs (also known as Curry-Howard correspondence), and the paradigm of proof-search-as-computation. In Geometry of Interaction, the processes (proves, via the Curry-Howard correspondence) are defined by their interactive behaviour. Thes framework is then especially well suited to the analysis of HOW the computation is performed, taking into account the procedural content of computation as well as the time of execution.

At a foundational level, the dynamical approach of Geometry of Interaction touches also the notion of truth. The logical definition of truth is not absolute, but closely linked with the interactive process. This approach opens fascinating connections with the point of view of Quantum Theory, and
calls for the exploration of the mathematical tools compatible with this major revolution.
The most recent version of Geometry of Interaction is developed within the setting of von Neumann algebra. We need now on one side to better understand and refine the theory, and on the other side to integrate the proof theoretical tools and notions (proof-nets, light linear logics) which are part of the novelties of Linear Logic; this will give us important tools to investigating and putting in use the potential of the framework, in particular to investigate a new structured approach to computational complexity, to expressiviness of programming languages, and to have new intuitions on computational models.

Project coordinator

Madame Claudia FAGGIAN (UNIVERSITE DE PARIS VII [DENIS DIDEROT]) – faggian@pps.jussieu.fr

The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.

Partner

PPS UNIVERSITE DE PARIS VII [DENIS DIDEROT]
LIPN UNIVERSITE DE PARIS XIII
IML CNRS - DELEGATION REGIONALE PROVENCE ET CORSE

Help of the ANR 396,406 euros
Beginning and duration of the scientific project: - 48 Months

Useful links