Baillot, Patrick and Mogbil, Virgile (LIPN) :  Soft lambda-calculus
<BR>
<BR>
Soft linear logic ([Lafont02]) is a subsystem of linear logic
characterizing the class PTIME. We introduce Soft
lambda-calculus as a calculus typable in the intuitionistic and
affine variant of this logic.  We prove that the (untyped) terms of
this calculus are reducible in polynomial time. We then extend the
type system of Soft logic with recursive types. This allows us to
consider non-standard types for representing lists.  Using these
datatypes we examine the concrete expressiveness of Soft lambda-calculus
with the example of the insertion sort algorithm.
<BR>
---------------
<BR>
De Carvalho, Daniel (IML, Marseille): 

Intersection types for Light affine lambda-calculus
<BR><BR>

Abstract: Light Affine Lambda Calculus is a term calculus for polynomial time computation.
 Some of the terms of Light Affine Lambda Calculus must however be regarded as errors. 
Intuitionistic Light Affine Logic (ILAL) types only terms without errors, but not all
 of them. We introduce two type assignment systems with intersection types : in the
 first one, typable pseudo-terms are exactly the terms without errors ; in the second
 one, they are exactly those that reduce to normal terms without errors.
<BR>
---------------
<BR>
Guiraud, Yves (IML, Marseille): Termination orders for operad presentations
<BR><BR>
Operad presentations, or Penrose diagrams rewrite systems, provide
 a framework in which commutative equational theories may have
 convergent presentations; the example of Z/2Z-vector spaces will
 be used. However, these objects require new tools, among them
 termination orders: one way to build some will be explained.
<BR>
-----
<BR>
 Marion, Jean-Yves (Loria - Ecole des Mines de Nancy) :
     Resource analysis by quasi-interpretations
<BR><BR>
Abstract :
We present a survey on methods to analyze the program
complexity, based on termination orderings and quasi-interpretations.
These methods can be implemented to certify the runtime (or memory,
stack size) of
programs.  This topic has some relations with the theory of algorithms
as we shall try to explain it.
This is a joint work with Guillaume Bonfante and Jean-Yves Moyen
(Loria).
<BR>
------------
<BR>
Moyen, Jean-Yves (LORIA, Nancy):
     Resource Termination -- using Petri Nets to analyse programs.
<BR><BR>
Programs written in a small assembly language are modelized by Petri Nets,
thus allowing many program analysis and transformation such as termination
analysis, deforestation or detecting non-size increasingness.
<BR>
----------
<BR>
Roversi, Luca (Torino) : Light logics and recursion 
<BR><BR>
The focus is about a work which is still under development.
The work is about the problem of increasing the number of algorithms that
can be programmed in paradigmatic programming languages with
predetermined complexity, derived from Linear Logic.
An experiment about how compositionally representing
  recursively defined
functions is presented.
The experiment will suggest to introduce a language that:<BR>
*) is  polytime normalizing under a lazy reduction strategy<BR>
*) allows, to use !-boxes that can depend on more than one assumption.
<BR>
---------------
<BR>
Terui, Kazushige (NII Tokyo): Proof nets and boolean circuits
<BR><BR>
Abstract:
We study the relationship between  
proof nets for mutiplicative linear logic 
(with unbounded fan-in logical connectives) and Boolean circuits.
We give simulations of each other in the style of the proofs-as-programs
correspondence; proof nets correspond to Boolean circuits 
and cut-elimination corresponds to evaluation. 
The depth of a proof net is defined to be the maximum logical depth 
of cut formulas in it,
and it is shown that every unbounded fan-in Boolean circuit
of depth n, possibly with st-conn2 gates, 
is polynomially simulated by a proof net of depth O(n) and vice versa.
Here, st-conn2 for 
st-connectivity gates for non-branching graphs.
Let APN^i be the class of languages for which
there is a polynomial size, log^i-depth family of proof nets.
We then have APN^i = AC^i(st-conn2).  
<BR>
---------------
<BR>
Vauzeilles, Jacqueline (LIPN):

AI problemes in the Horn Linear logic: semantics and complexity
<BR>
<BR>
The typical AI problem of making a plan of the actions to be performed
by a robot so that it could get into a set of final situations, if it
started with a certain initial situation, is generally very complex. We
introduce Horn linear logic as a comprehensive logical system capable
of handling the typical AI problem of making a plan, and the planning problem
under uncertainty about the effects of action is proved to be EXPTIME-complete.
The planning complexity is reduced to PSPACE for the robot systems with only 
pure deterministic actions.<BR>
A particular interest of our results is focused on planning problems with an 
unbounded number of functionally identical objects: by means of replacing the 
unbounded number of specific names of objects with one generic name, we contract 
thereby the exponential search space over 'real' objects to a small polynomial
search space but over the 'generic' one, and solutions are proved to be directly
translatable into polytime solutions to the original planning problem.