TMR LINEAR Scientific description

The network research work is organized along four main axes which as described below.

Proof theory

Linear logic was invented by Girard as a refinement of classical and intuitionistic logic, characterized by the splitting of standard connectives (``and'' and ``or'') in two classes (additive and multiplicative) and the introduction of new connectives (exponentials) which give a logical status to the operations of erasing and copying (corresponding to the ``structural rules'' of classical and intuitionistic sequent calculi). This change of viewpoint on structural operations has many striking consequences in proof theory, among which one of the most important is the introduction of proof-nets, a graph-theoretic presentation that gives a more geometric account of proofs. Our main goals in the theme ``proof theory of linear logic'' can be summarized as follows:

Additive proof-nets.

The theory of multiplicative-exponential proof nets is well established, but its extension to the additive fragment has been for a long time a challenging problem. Partial, and thus unsatisfying, solutions have been proposed by Girard. The recent development of the theory of free bicompletion of categories by Joyal suggests that new advances are now possible on this topic.

Feasible arithmetics.

By adding some logical constraints to linear logic, one can obtain subsystems in which only polynomial time (LLL) or elementary time functions (ELL) can be programmed. This result has enormous potential for theoretical applications. One idea is to formulate arithmetic inside these systems in order to obtain refinements of usual results in proof theory and complexity.

Non commutative linear logic.

Non commutative linear logic appears for the moment as a topic in which very little is understood. Fleury showed that the analysis of the exchange rule can use tool from algebraic topology (knot theory, braided groups, ...). This needs further improvements, particularly in relation with, e.g., Abrusci's work on non commutative proof-nets.

Semantics

The goal of semantics is to give a ``mathematical'' counterpart to syntactical devices such as proofs and programs, thus bringing to the fore their essential properties: it expresses the meaning of syntax. It maps the concrete syntactical objects to an algebraic, geometric, categorical... description, which is easier to grasp, stresses basic invariants and, sometimes, eventually results in improvements of the syntax: linear logic itself comes from a denotational model of second order intuitionistic propositional logic. Semantics of proofs and programs divides in two parts: static models where proofs are basically interpreted by functions and cut-elimination by composition, and dynamic models which give a much more informative account of cut-elimination.

Unification, static vs. dynamic.

It seems now at hand that static and dynamic models be classified in a uniform framework. Such an achievement would greatly clarify the theory, and possibly would also have some resonance in the concurrency field. Two approaches will be developped:

Game semantics. The connection between game semantics and the geometry of interaction is now almost completely clarified. Some results already exist relating games and denotational models (e.g., sequential algorithms and hypercoherences) which lead to think that a more general framework could be set.

Linear algebra. From the beginning linear logic has privileged connections with linear algebra. Current work in progress tries to exploit this relation for building a model, which would be both denotational and dynamical, using techniques from functional analysis.

Denotational semantics.

This is a wide field of research. Let us mention a few important issues. In domain theory and the semantics of programming languages, linear logic has been influential in drawing the focus away from cartesian closed category of domains to the more finely tuned categories which model linear logic. The basic goal here is the development of a theory of categories with duality, providing general tools for constructing models and comparing them. Another important issue is the use of the linear decomposition of intuitionistic implication for building models of call-by-value lambda-calculus. Last example: Girard has proposed the use of Banach spaces for modelling linear logic. This is an interesting track to follow for connecting linear logic to more traditional fields of mathematics.

Game semantics.

Since the invention of game models that solved the full abstraction problem for PCF, game semantics has proved to be a very flexible tool for modelling the dynamics of programming languages. However a lot of questions remain unanswered and particularly it has to be understood how this semantics which works so well for intuitionistic linear logic can be extended to the classical case.

Abstract geometry of interaction.

The geometry of interaction was originally designed for non-additive proof-nets. A crucial notion in the definition of the latter is that of a boxe, a kind of synchronization device in the syntax for manipulating arbitrarily big pieces of code as a whole. In some sense the geometry of interaction is a localization of the cut-elimination procedure. An interesting question is to generalize the geometry of interaction to other frameworks than proof-nets with boxes, e.g., Milner's action calculi. The goal would be to characterize those syntaxes for which abstract geometry of interaction models can be built.

Concurrency

The problem of finding a convincing mathematical theory of concurrent processes is one of the most important and challenging in computer science. Linear logic is thought from the very beginning as having some connections with this problem, but its contributions are still to be developped. Here are three directions of research.

Categorical models for concurrency.

Linear logic is coming to play an important role in a categorical approach to models for concurrency. Work of Winskel, Joyal and Nielsen on a general approach to bisimulation through open maps led to a model of classical linear logic which might be central in extending bisimulation to higher-order features (such as process passing in process calculi).

Proof-nets and concurrency.

Since the invention of proof-nets, it has been clear that the cut-elimination procedure, especially when described by the geometry of interaction, is sufficiently local to be performed asynchronously. This idea is fundamental in the invention of interaction nets by Lafont. At this point it is natural to ask whether proof-nets and geometry of interaction might be realistically turned into a fundational theory of concurrent calculi.

Applications

More concrete goals will be aimed at:

Linearity analysis and type synthesis.

Work of Danos, Joinet and Schellinx has initiated the use of linear logic as a kind of ``typing system'' for intuitionistic or classical proofs: the idea here is to decorate the proofs by as few exponential connectives as possible in order to gain the best possible control on memory management. On the other hand, Bierman, Bräuner, Ronchi della Rocca,... have proposed linear versions of typed lambda-calculi aiming at controlling the use of resources by means of linear typing constraints. We want to derive from this work some applications towards the synthesis of linear types for functional languages, in the spirit of ML, but more informative from the operational point of view.

Analysis of the complexity of sharing reductions.

The geometry of interaction has proved to be a useful tool in applied topics, e.g., sharing reductions, interaction nets. In particular some implementations have already been realised, e.g., an algorithm for sharing reduction due to Asperti (Bologna). However a lot of optimization work remains to be done, from the theoretical point of view in refining the design of the algorithm, as well as from the practical point of view, for example in the choice of the implementation language.

Logic programming.

It is a long standing paradigm of computation to consider formulae as processes and proof search as execution. The fine grain decomposition of connectives provided by linear logic allows for the design of logic programming languages that are much more expressive than those based on traditional logic. Applications to parallel programming, database query languages, AI and linguistics have been investigated and have to be developped further.