Séminaire, 16 octobre 2014
Programme
- 10:30 – 12:00
-
Sylvain Schmitz (LSV, ENS Cachan)
The ties between propositional linear logic on the one hand and extensions of vector addition systems on the other hand have long been known, as they lie for instance at the heart of Lincoln et al.'s 1992 undecidability proof. With Ranko Lazić we recently revisited these connections with an eye on complexity issues, which allowed us to prove tight complexity bounds on provability in affine and contractive fragments of linear logic. Our work also yields a new Tower lower bound on provability in MELL, for which decidability is still open.
Work presented at CSL-LICS 2014; full paper available on arXiv: http://arxiv.org/abs/1401.6785.
- 14:00 – 15:00
-
Paulin Jacobé de Naurois (CNRS - Univ. Paris 13)
We define Vector Addition with States and Split/Join Transitions, a new model that extends VASS. Non-negative reachability in this model without join transitions is known to be equivalent to the decidability of MELL, and to be TOWER-hard. As a first step towards a reachability result, we define a suitable notion of covering graph for the model, and prove its finiteness and effective constructibility.
- 15:30 – 16:30
-
Flavien Breuvart (PPS (Paris 7))Invited talk: De la caractérisation des modèles de H*
Je ferai une présentation rallongée de l'article LICS du même nom.
Il s'agit de donner une caractérisation, pour une classe importante de modèles du lambda-calcul non typé, de la pleine adéquation pour la normalisation de tête (i.e. pour H*). On montrera en effet qu'il est pour cela nécessaire et suffisant d'être hyperimmune. L'hyperimmunité est une notion que nous introduirons qui demande à ce que les comportements mal fondés du modèle ne soient pas capturables par des fonctions récursives.
Ce résultat sera notamment utilisé comme prétexte et exemple pour l'introduction d'un outil central dans ma thèse: les lambda-calculs avec tests. Il s'agit d'enrichir le lambda-calcul non typé avec des opérateurs directement issus du modèle dénotationnel impliqué afin de rendre celui-ci pleinement adéquat pour notre nouvelle syntaxe. Intuitivement, ces opérateurs vont internaliser un processus d'inférence de type possiblement divergent qui tente de typer l'arbre de Böhm d'un terme.
