Institut de Mathématiques de Luminy
SÉMINAIRES 2008
Logique et Interactions

Organisateurs :
Yves Lafont (tél. 04 91 26 96 37)
Emmanuel Beffara (tél. 04 91 26 96 35)
Lieu : IML, Bâtiment TPR2- CNRS :
Salle de Séminaires : 3ème étage (304-306).
Horaire : en règle générale le jeudi, à 14h.

jeudi 18 décembre
Olivier Laurent (LIP, ENS Lyon) :
Game semantics for first-order logic

Abstract: We refine HO/N game semantics with an additional notion of pointer (μ-pointers) and extend it to first-order classical logic with completeness results. We use a Church style extension of Parigot’s λμ-calculus to represent proofs of first-order classical logic. We present some relations with Krivine’s classical realizability and applications to type isomorphisms.

jeudi 13 novembre
Christine Tasson (PPS, Univ. Paris 7) :
Totalité algébrique et complétude

Résumé : Les espaces de finitude forment un modèle catégorique de la logique linéaire dont les objets sont des espaces vectoriels topologiques et les morphismes des applications linéaires continues. En essayant de généraliser les espaces de finitude, nous avons défini une notion naturelle de totalité qui permet de définir un modèle de la logique linéaire plus fin que celui des espaces de finitude. Ainsi, nous pouvons espérer prouver un théorème de complétude pour un lambda-calcul avec une somme barycentrique et des constructions booléennes.
Cet exposé débutera avec l'étude d'un lambda-calcul barycentrique booléen. Après en avoir introduit un modèle utilisant des polynômes, je présenterai un théorème de complétude pour ce calcul. Dans un second temps, je définirai les espaces de finitude et la totalité qui nous ont amenés à considérer ce théorème.

jeudi 23 octobre
Joachim de Lataillade (IML) :
Jeux et système F à la Curry

mercredi 18 juin
à 10h

Damiano Mazza (PPS, Univ. Paris 7) :
Sur l'expressivité des réseaux d'interaction
et de leurs variantes non-déterministes

Résumé : Quels types de processus de calcul peut-on exprimer dans les réseaux d'interaction ?
On analysera cette question à l'aide des structures d'événements, un outil qui permet de décrire assez précisement plusieurs aspects fondamentaux de la structure dynamique d'un processus calculatoire (e.g. causalité, parallélisme, non-déterminisme). On trouvera ainsi un nombre de résultats, principalement négatifs, concernant l'expressivité des réseaux d'interaction et de leurs variantes non-déterministes. Notamment, on verra qu'il n'existe pas de codage suffisamment "fidèle" du pi-calcul dans les réseaux d'interaction différentiels.

mardi 17 juin
séance reportée

Paolo di Giamberardino (Université Roma 3) :
Pointed sets: How to semantically characterize jumps

Abstract: In our PhD thesis, we introduced a new class of multiplicative/additive proof nets, J-proof nets, which are a typed version of Faggian and Curien's L-nets. The distinctive feature of J-proof nets with respect to other proof nets syntaxes, is the possibilty of representing proof nets which are partially sequentialized, by using jumps (that is untyped extra edges) as sequentiality constraints. Usually, from a semantical point of view (for instance in relational and coherent semantics) jumps are "invisible"; adding jumps on a proof net does not modify its semantics. We propose an extension of relational semantics called pointed semantics, which allows to semantically characterize jumps, and we prove the injectivity of this model with respect to J-proof nets.

jeudi 5 juin
Marc de Falco (IML, Marseille) :
The geometry of interaction
of differential interaction nets

Abstract: The Geometry of Interaction purpose is to give a semantic of proofs or programs accounting for their dynamics. The initial presentation, translated as an algebraic weighting of paths in proofnets, led to a better characterization of the lambda-calculus optimal reduction. Recently Ehrhard and Regnier have introduced an extension of the Multiplicative Exponential fragment of Linear Logic (MELL) that is able to express non-deterministic behaviour of programs and a proofnet-like calculus: Differential Interaction Nets.
This paper constructs a proper Geometry of Interaction (GoI) for this extension. We consider it both as an algebraic theory and as a concrete reversible computation. We draw links between this GoI and the one of MELL. As a by-product we give for the first time an equational theory suitable for the GoI of the Multiplicative Additive fragment of Linear Logic.

jeudi 29 mai
Virgile Mogbil (LIPN, Univ. Paris 13) :
NL-complétude de la correction M(E)LL
(en collaboration avec P. Jacobé de Naurois)

Résumé : Je donnerai un nouveau un critère de correction très simple pour les structures de preuves de MLL (et par extension, de MELL). Avec ce n-ième critère nous prouvons que décider la correction de ces structures de preuves est NL-complet.

mercredi 7 mai
Colin Riba (INRIA Sophia-Antipolis) :
Unions of reduciblity families
for lambda-calculus and rewriting

Abstract: The most flexible strong normalization proofs methods for various extensions of typed lambda-calculi use type interpretations. Among them we distinguish Girard's reducibility candidates, Tait's saturated sets and interpretations based on biorthogonality. In this talk we compare these different interpretations wrt their ability to handle rewriting and to their stability by union.
We first propose a generalization of the notion of neutral term in Girard's candidates which allows to define candidates in a generic way. Concerning stability by union, we recall that there are confluent typed rewrite systems that do not admit stable by union type interpretations. We present a necessary and sufficient condition for Girard's candidate to be stable by union and a necessary and sufficient condition for the closure by union of biorthogonals to be reduciblity candidates. The second condition is strictly more general than the first one, and allows to define Tait's saturated sets for rewriting in a uniform way. Moreover, we show that for orthogonal constructor rewriting, Girard's candidates are stable by union.

jeudi 13 mars
Christophe Fouqueré (Univ. Paris 13) :
Comment la ludique vient au web :
une autre lecture d'opérations usuelles

Résumé : Le web (sous l'angle de sites ou de services) apparaît comme un cadre trivial d'interaction. En définir une interprétation en termes de la ludique de J.-Y. Girard peut se poser, avec l'objectif concret de mieux savoir définir les types associés aux programmes en jeu (donc de leur contrôle). Nous indiquerons comment interpréter le cadre des sites web en termes d'interaction, nous rappellerons comment passer des services web via les processus CCS à des arbres d'actions, puis à une reconstruction des types en ludique. Nous nous attarderons sur quelques éléments spécifiques liant théorie et pratique : non uniformité (bouton back ou reload !), asymétrie (client-serveur).

jeudi 28 février
Thierry Cachat (Univ. Paris 7) :
Les automates d'arbres facilitent la théorie des ordinaux

Résumé : On propose une nouvelle démonstration, plus simple et avec une meilleure complexité, de la décidabilité de la logique du premier ordre de (omega^{omega^i},+) et de la logique monadique du second ordre de (omega^i,<). Notre algorithme utilise les automates d'arbres et une nouvelle représentation des (ensembles d') ordinaux par des arbres (infinis). On donnera des extensions à certains ordres linéaires dispersés.

jeudi 7 février
Giulio Manzonetto (Univ. Paris 7 & Univ. Cà Foscari) :
Modèles non concrets du lambda-calcul

Résumé : Les modèles du lambda-calcul pur peuvent être définis soit comme des objets réflexifs dans des catégories Cartésiennes fermées (modèles catégoriques) soit comme des algèbres combinatoires satisfaisant les cinq axiomes de Curry et l'axiome de Meyer-Scott (lambda-modèles). En ce qui concerne les modèles catégoriques, on montre que tout modèle catégorique peut être présenté comme un lambda-modèle, même si la ccc (catégorie Cartésienne fermée) sous-jacente n'a pas assez de points, et on donne des conditions suffisantes pour qu'un modèle catégorique vivant dans une ccc ``cpo-enriched'' arbitraire ait H* pour théorie équationnelle. On construit un modèle catégorique qui vit dans une ccc d'ensembles et relations (sémantique relationnelle) et qui satisfait ces conditions. De plus, on montre que le lambda-modèle associé possède des propriétés algébriques qui le rendent apte à modéliser des extensions non-déterministes du lambda-calcul.

jeudi 17 janvier
Sylvain Salvati (LaBRI, INRIA, Bordeaux) :
Quelques réductions à la décidabilité du fragment multiplicatif et exponentiel de la logique linéaire

Résumé : Nous présentons une notion d'automate d'arbres dont l'ambition est d'étudier la décidabilité du fragment multiplicatif et exponentiel de la logique linéaire (MELL). Ces automates, "automates d'arbres d'addition de vecteurs" (VATA) (de Groote, Guillaume, Salvati 2003), peuvent se voir comme une extension pour les arbres des automates d'additions de vecteurs (VAS) qui ont servi à Kosaraju pour démontrer la décidabilité du problème de l'accessibilité dans les réseaux de Petri. Du fait que l'obtention des VATA à partir des VAS est similaire à l'obtention de la notion d'automate d'arbres à partir des automates d'états finis pour les mots, les VATA sont une notion naturelle d'automate. Nous esquisserons la démonstration du fait que le problème de la vacuité du langage d'un VATA est Turing-équivalent à l'existence d'une démonstration pour un séquent de MELL.
Les techniques mises en oeuvre par Kosaraju concernant les VAS ne s'étendent pas immédiatement aux VATA. Cependant les VATA permettent de faire simplement le lien entre la décidabilité de MELL et celles d'autres problèmes. Nous montrerons à titre d'exemple comment les VATA permettent de montrer que la décidabilité des grammaires minimalistes (Stabler 96) est équivalente à celle de MELL.

EL, le 10 décembre 2008