6th meeting: June, 8, 2011 at LORIA, Nancy

* 6th meeting of the COMPLICE project *

Date : Wednesday, June 8th 2011.

Location : LORIA, Nancy.

Access instructions (See the reception desk)

Invited speaker: Pierre Letouzey (Paris PPS)

Invited speaker: Daniel Leivant (Nancy/Bloomington)

Preliminary program:

Abstracts:

 Pierre Letouzey (PPS) (invité). TBA.

 Marc Lasson (Lyon). Controlling program extraction in light logics

We present two refinements, based on program extraction in elementary affine logic and light affine logic, of Krivine & Leivant’s system FA2 . This system allows higher-order equations to specify the computational content of extracted programs. The user can then prove a generic formula, using these equations as axioms. The system guarantees that the extracted program satisfies the specification and normalizes in elementary time (for elementary affine logic) or polynomial time (for light affine logic). Finally, we show that both systems are complete with respect to elementary time and polynomial time functions.

 Matthieu Perrinel (Lyon). Système de type basé sur la logique linéaire par niveaux

La logique linéaire light par niveau, introduite par Baillot et Mazza, est un sur-système de la logique linéaire light de Girard (LLL). Une des versions, permettait d’exprimer exactement les fonctions de Ptime, sans recourir à la modalité §. Cependant, il n’y avait aucune borne sur la longueur des réductions. Dans cet exposé, nous présenterons un système de type basé sur la logique linéaire light par niveau, vérifiant la subject reduction et normalisant en temps polynomial.

 Daniel Leivant (Nancy) (invité). TBA.

 Damiano Mazza, Ugo dal Lago, Tobias Heindel. Towards a theory of computational complexity for concurrent processes.

We present a first set of ideas whose aim is to build a theory of computational complexity capable of meaningfully addessing concurrent, instead of purely functional, computation. We start by defining the complexity of "behaviors" (which replace functions), technically represented by labelled transition systems modulo coupled simulation. This is done by considering a simple, Turing-complete, asynchronous, CCS-based concurrent calculus, and defining a notion of computational cost using its interpretation in event structures. Then, we give a few tentative definitions of complexity classes, some of which should correspond to "usual" classes (P, NP, NC...).

 Jean-Yves Marion (Nancy). A type system to analyse complexity of imperative language.

We propose a type system for an imperative programming language, which certifies program time bounds. This type system is based on secure flow information analysis. Each program variable has a level and we prevent information from flowing from low level to higher level variables. We also introduce a downgrading mechanism in order to delineate a broader class of programs. Thus, we propose a relation between security-typed language and implicit computational complexity. We establish a characterization of the class of polynomial time functions.

 Antoine Madet (PPS). An elementary affine λ-calculus with multithreading and side effects.

Linear logic provides a framework to control the complexity of higher-order functional programs. We present an extension of this framework to programs with multithreading and side effects focusing on the case of elementary time. Our main contributions are as follows. First, we provide a new combinatorial proof of termination in elementary time for the functional case. Second, we develop an extension of the approach to a call-by value λ-calculus with multithreading and side effects. Third, we introduce an elementary affine type system that guarantees the standard subject reduction and progress properties. Finally, we illustrate the programming of iterative functions with side effects in the presented formalism.