Complice project

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

Programme à venir.

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

Programme à venir.

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

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).

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

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

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.

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

Workshop DICE 2012

Patrick Baillot — 2011-09-09T09:35:19Z

The 3rd edition of the workshop Developments in Implicit Computational complExity (DICE 2012) will be part of ETAPS 2012 :

http://dice2012.cs.unibo.it/

March 31st and April 1st, 2012, Tallinn, Estonia

Workshop DICE 2012

Patrick Baillot — 2011-09-09T09:33:16Z

The 3rd edition of the workshop Developments in Implicit Computational complExity (DICE 2012) will be part of ETAPS 2012 :

http://dice2012.cs.unibo.it/

March 31st and April 1st, 2012, Tallinn, Estonia

Post-Doc position at LORIA, Nancy

Patrick Baillot — 2011-09-01T14:52:45Z

Post-doctoral position at Nancy University, INRIA-LORIA, France

on Implicit computational complexity (ICC)

Applications are now invited for a postdoctoral position on ICC. Candidates are expected to contribute to research within the ANR project COMPLICE. The ideal candidate will have interest on type systems, logics, and complexity. The position is for one year. The start date is negotiable.

To be considered for this position, please send a CV, list of publications, a brief statement of interest, and the names of two references to Jean-Yves Marion (Jean-Yves.Marion@loria.fr). Further inquiries—for example, questions about specific project topics—are also welcome.

COMPLICE is a four-year project whose partner sites are ENS Lyon, Université Paris 13 and LORIA-Nancy. The project's goal is to investigate the foundations and applications of implicit computational complexity (ICC), along the lines of semantics and logic, functional programming, program extraction from proofs, quantitative properties and ICC for concurrent systems.

http://www.loria.fr/

http://en.inria.fr/inria-research-c...

http://www-lipn.univ-paris13.fr/com...

Postdoctorat au LORIA, Nancy

Patrick Baillot — 2011-09-01T14:51:24Z

Post-doctoral position at Nancy University, INRIA-LORIA, France

on Implicit computational complexity (ICC)

http://www.loria.fr/

http://en.inria.fr/inria-research-c...

http://www-lipn.univ-paris13.fr/com...