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

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

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.