8e réunion : 31/05/2012, ENS Lyon

8e Réunion de projet : Jeudi 31/05/2012, ENS Lyon

Lieu : ENS Lyon, LIP, Amphi A, 3e étage

Accès (Enter at 46 allée d’Italie, that is to say below the big "arch" ; there is a reception desk)

Access map

Preliminary programme :

Abstracts :

 J.-Y. Marion et R. Péchoux (Loria Nancy). Complexity Information Flow in a Multi-threaded Imperative Language.

Abstract. We propose a type system to analyze the time consumed by multi-threaded imperative programs with a shared global memory, which delineates a class of safe multi-threaded programs. We demonstrate that a safe multi-threaded program runs in polynomial time if (i) it is strongly terminating wrt a non-deterministic scheduling policy or (ii) it terminates wrt a deterministic and quiet scheduling policy. As a consequence, we also characterize the set of polynomial time functions. The type system presented is based on the fundamental notion of data tiering, which is central in implicit computational complexity. It regulates the information flow in a computation. This aspect is interesting in that the type system bears a resemblance to typed based information flow analysis and notions of non-interference. As far as we know, this is the first characterization by a type system of polynomial time multi-threaded programs.

 E. Hainry, J.-Y. Marion et R. Péchoux (Loria Nancy) : A Characterization of Polynomial Space with Forks.

We introduce a type system for a parallel imperative language using while-loops and fork/wait instructions in order to analyze the (parallel) time and (sequential) space complexity. The type system provides an analysis of the data-flow based on a data ramification principle and it is related to secure typed languages. The main result states that well-typed programs characterize exactly the set of functions computable in polynomial space under termination, confluence and lock-freedom assumptions. More precisely, each process computes in polynomial time so that the evaluation of a process may be performed in polynomial time on a parallel model of computation.

 Matthieu Perrinel (LIP Lyon). Towards intensionally complete linear logic subsystems for polynomial and elementary time

All previously studied subsystem of linear logic characterizing Ptime lacked expressive power. Although every Ptime function can be computed in those systems, they do not always accept usual algorithms. In this work we will use the context semantics of Dal Lago to approach the "expressivity frontier" : the sets of programs that could be accepted by Ptime sound "reasonable" linear logic subsystem.

 Patrick Baillot (LIP Lyon) et Ugo Dal Lago (Bologne)

Polynomial interpretations and their generalizations like quasi-interpretations have been used in the setting of first-order functional languages to design criteria ensuring statically some complexity bounds on programs. This fits in the area of implicit computational complexity, which aims at giving machine-free characterizations of complexity classes. Here we extend this approach to the higher-order setting. For that we consider the notion of simply typed term rewriting systems, we define higher-order polynomial interpretations (HOPI) for them and give a criterion based on HOPIs to ensure that a program can be executed in polynomial time. In order to obtain a criterion which is flexible enough to validate some interesting programs using higher-order primitives, we introduce a notion of polynomial quasi-interpretations, coupled with a simple termination criterion based on linear types and path-like orders.