Complice project

Workshop DICE 2013

Patrick Baillot — 2012-11-13T09:26:59Z

The 4th workshop Developments in Implicit Computational complExity (DICE 2013) will take place in Rome, as part of ETAPS 2013 :

http://dice2013.di.unito.it/

March 16th-17th, 2013.

Workshop DICE 2013

Patrick Baillot — 2012-11-13T09:26:11Z

The 4th workshop Developments in Implicit Computational complExity (DICE 2013) will take place in Rome, as part of ETAPS 2013 :

http://dice2013.di.unito.it/

March 16th-17th, 2013.

9th project meeting: 29/11/2012, Univ. Paris 13

Virgile Mogbil — 2012-10-05T14:46:13Z

- Meetings

9ème réunion de projet : 29/11/2012, Univ. Paris 13

Virgile Mogbil — 2012-10-05T14:46:10Z

- Rencontres

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

Patrick Baillot — 2012-04-25T11:01:35Z

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 :

10h15	ACCUEIL
10h30	J.-Y. Marion (Nancy). Complexity Information Flow in a Multi-threaded Imperative Language (travail avec Péchoux).
11h15	A. Madet (Paris). A polynomial lambda-calculus with concurrency and side effects.
12h	Pause-déjeuner
14h	R. Péchoux. (Nancy). A Characterization of Polynomial Space with Forks (travail avec Hainry et Marion).
14h45	M. Perrinel (Lyon). Towards intensionally complete linear logic subsystems for polynomial and elementary time.
15h30	P. Baillot (Lyon). Higher-order interpretations and program complexity (travail avec Dal Lago).
16h15	pause-café
16h45	discussion de projet
17h30	FIN

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-ﬂow based on a data ramiﬁcation 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, conﬂuence 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.

8th meeting: 31/05/2012, ENS Lyon

Patrick Baillot — 2012-04-25T10:59:40Z

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:

10h15	ACCUEIL
10h30	J.-Y. Marion (Nancy). Complexity Information Flow in a Multi-threaded Imperative Language (travail avec Péchoux).
11h15	A. Madet (Paris). A polynomial lambda-calculus with concurrency and side effects.
12h	Pause-déjeuner
14h	R. Péchoux. (Nancy). A Characterization of Polynomial Space with Forks (travail avec Hainry et Marion).
14h45	M. Perrinel (Lyon). Towards intensionally complete linear logic subsystems for polynomial and elementary time.
15h30	P. Baillot (Lyon). Higher-order interpretations and program complexity (travail avec Dal Lago).
16h15	pause-café
16h45	discussion de projet
17h30	FIN

Abstracts:

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

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

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

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

Complexity Winter School @LI2012

Patrick Baillot — 2012-02-17T12:13:56Z

See: http://li2012.univ-mrs.fr/programme/week1/

Complexity Winter School @LI2012

Patrick Baillot — 2012-02-17T12:13:50Z

See : http://li2012.univ-mrs.fr/programme/week1/

7th project meeting: 1/12/2011, Univ. Paris 13

Patrick Baillot — 2012-02-17T12:10:46Z

7e Réunion de projet : Jeudi 1/12/2011, Univ. Paris 13, LIPN.

Lieu : Université Paris 13, salle D214 (bâtiment en face du LIPN, 2ème étage : couloir accessible uniquement avec un BADGE)

(Entre les bâtiments G en B sur le plan suivant http://www-lipn.univ-paris13.fr/pla...)

Invité : Merci à Ugo Dal Lago (Univ. Bologne).

Programme

10h15	ACCUEIL
10h30	Work in progress, Ugo Dal Lago (Univ. Bologne)
11h30	PAUSE
11h45	Linear Logic by Asymmetric Levels, Andrei Dorman (LIPN)
12h15	Bornes fortes pour la logique linéaire par niveau, Matthieu Perrinel (ENS Lyon)
12h45	REPAS
14h15	A computational model for measuring the complexity of concurrent processes, Damiano Mazza (LIPN)
15h00	Terminaison dans les processus d'ordre supérieur, Simon Castellan (ENS Lyon)
15h30	PAUSE
15h45	A probabilistic operational semantics for the Lambda Calculus (and some considerations on Probabilistic ICC), Margherita Zorzi (LIPN)
16h15	DISCUSSION DE PROJET
16h45	FIN

Résumés

Titre : Linear Logic by Asymmetric Levels, Andrei Dorman (LIPN).

Résumé : We give a new linear logic system bounded in complexity for deterministic polytime functions. Girard's result, concerning elementary and light linear logic, characterizes this class of functions by introducing a stratification principle on proofs, using a notion of depth. Mazza and Baillot have generalized that principle. They propose a general form of stratification, based on inducing levels in proof-nets by means of indexes, which allows them to extend Girard's system while keeping the same complexity properties. We now propose an evolution of this system, with a greater acceptance of nets as proof-nets than in Baillot and Mazza's L^4 and show that it characterizes the polynomial time complexity class.

Titre : Bornes fortes pour la logique linéaire par niveau, Matthieu Perrinel (ENS Lyon).

Résumé : La logique linéaire par niveaux, introduite par Baillot et Mazza, est un sursystème de la logique linéaire light de Girard. Des bornes polynomiales faibles, c'est à dire pour des stratégies de réduction particulières, ont été montrées pour deux versions de la logique linéaire par niveau (mL4 et mL4_0). Mais, les stratégies correspondant étant complexe, il était difficile de transformer ces logiques en vrais langages de programmation, avec une stratégie de réduction explicite. En étendant la sémantique des contextes à la logique linéaire par niveaux, nous montrons une borne forte polynomiale (valable pour n'importe quelle stratégie de réduction) pour mL4 et mL4_0.

Titre : Terminaison dans les processus d'ordre supérieur, Simon Castellan (ENS Lyon).

Résumé : Dans cet exposé, nous étudions un calcul résultant de la fusion du pi-calcul et du lambda-calcul. Nous proposons un système de types qui garantit la terminaison dans ce calcul, et nous proposons un sous-calcul qui permet de garantir une borne sur la longueur des réductions.

Titre : A computational model for measuring the complexity of concurrent processes, Damiano Mazza (LIPN), joint work in progress with Ugo Dal Lago, Tobias Heindel, and Daniele Varacca.

We present a model of concurrent computation which is based on a multi-processor machine, with private memory, asynchronous communication between processors, and an interface with which the machine may perform input/output with the external world. Such a machine may execute CCS/pi-calculus hybrid processes, and therefore implement concurrent behaviors, extending the functional behaviors of traditional Turing machine/recursive theory. Our machine has an obvious space cost model (based on the amount of memory used and messages exchanged); less trivially, we show how a time cost model may be defined, based on trace semantics (equivalent to event structures).

Titre : A probabilistic operational semantics for the Lambda Calculus (and some considerations on Probabilistic ICC), Margherita Zorzi (LIPN).

In the main part of this talk we will present some ideas about probabilistic operational semantics for a non-deterministic extension of pure lambda calculus. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics are both inductively and co-inductively defined. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by-value and in call-by-name. The classical Plotkin's simulation between strategies is finally revisited in the probabilistic setting. We will conclude the talk with a brief discussion about probabilistic complexity theory and possible research directions about Probabilistic ICC.

7e Réunion de projet: 1/12/2011, Univ. Paris 13

Virgile Mogbil — 2011-10-17T09:49:52Z