Institut de Mathématiques de Luminy
SÉMINAIRES 2005
Logique de la Programmation (LDP)

Organisatrice :

Marie-Renée Fleury-Donnadieu (téléphone : 04 91 26 96 38).
Lieux : IML, Bâtiment TPR2- CNRS : Amphithéatre de l'IML : 1er étage (130-134)
Salle de DEA et salle de réunion de l'équipe : 2ème étage
Salle de Séminaire : 3ème étage (304-306).
Horaire : en règle générale le lundi, à 14h.

mardi 13 décembre
----- à 10 h -----
amphithéâtre Herbrand

Marcelo Fiore (
Computer Lab., Univ. Cambridge) :
Titre à préciser.

Résumé : http://iml.univ-mrs.fr/ldp/Seminaire/SemLog0506.html

lundi 12 décembre
----- à 10 h -----
amphithéâtre Herbrand

Thomas Streicher (
Technische Univ. Darmstadt) :
Titre à préciser.

Résumé : http://iml.univ-mrs.fr/ldp/Seminaire/SemLog0506.html

lundi 28 novembre
----- à 14 h -----
amphithéâtre Herbrand

Daniel De Carvalho (
IML) :
Sémantiques non uniformes du lambda-calcul, types avec intersection et temps de calcul.

Résumé : http://iml.univ-mrs.fr/ldp/Seminaire/SemLog0506.html

mardi 20 septembre
----- à 14 h -----
amphithéâtre Herbrand

Kazushige Terui (
Keio university, Japon- Invité IML) :
Towards a semantic characterization of cut-elimination.
(joint work with Agata Ciabattoni).

Résumé : http://iml.univ-mrs.fr/ldp/Seminaire/SemLog0506.html

lundi 19 septembre
----- à 14 h -----
amphithéâtre Herbrand

Peter Hines (
Oxford University, UK) :
Conditional iteration in quantum systems.
(joint work with Philip Scott).

Résumé : http://iml.univ-mrs.fr/ldp/Seminaire/SemLog0506.html

mardi 5 juillet
----- à 14 h -----
amphithéâtre Herbrand

Juliusz Chroboczek (
PPS - Univ. Paris 7) :
CPC, Un dialecte concurrent du « C »
implémenté par passage de continuations.

Résumé : Les programmes sont parfois vus comme des processus qui lisent une quantité finie de données, puis produisent un résultat. La plupart des programmes qu'on manipule, cependant, n'obéissent pas à cette discipline « batch »: ils interagissent avec leur environnement tout au long de leur exécution. Ce sont des systèmes réactifs, ou programmes concurrents.
Il existe deux techniques pour écrire des programmes concurrents: l'utilisation de processus multiples (threads), et la programmation par boucle à évènements (event loop, ou event-driven state machine). La première est gourmande de ressources (surtout de mémoire), la seconde est très difficile à mettre en oeuvre.
À cet exposé, je montrerai comment la transformation par passage de continuations (CPS) permet de convertir automatiquement du code à threads en code à boucle à évènements. Je montrerai ensuite comment la CPS, classiquement définie pour le lambda-calcul et ses extensions, peut s'appliquer au langage de programmation « C ».
Il existe une implémentation de ce travail -- appelée « CPC » --, et je conclurai mon exposé par quelques mesures d'efficacité.

jeudi 2 juin
----- à 14 h -----
salle de séminaires

Masahiro Hamano (JAIST-invité
IML) :
Hypercoherence Completion of Cographs.

Résumé : This talk concerns denotational semantics for polarized MALL (MALLP). In a joint work with Phil Scott, we studied that Ehrhard's hypercoherences provide a categorical model for MALLP. This was done by constructing adjoint functors to change polarities between positive and negative sub-categories of hypercoherences such that fixed point sub-category of the adjunction coincides with Girard's coherent spaces.
In this talk, we attempt to refine this hypercoherence model of MALLP by using structure of cographs at its base. Cographs were studied in connection with linear logic by Ehrhard under the name of parallel and serial hypercoherences ('00) and we interpret polarity change operators by special kinds of parallel and serial graph constructions. We interpret morphisms between same polarities by invariant maps with respect to permutations of components for serial-parallel graphs. On the other hand 2-softness of cographs yields an interpretation of morphisms from positive to negative.
Then our model is obtained by hypercoherence completion of these graphs, whose completion is a straightforward generalization of Hu-Joyal's coherence completion ('99) where each vertex of a web is replaced by an object of a category.
We furthermore discuss polarized softness and focalization property for the model so obtained.

mardi 31 mai
----- à 14 h -----
salle de séminaire

Jean-Marc Andreoli (Xerox-
IML),
Gabriele Pulcini
(Univ. Rome 3-
IML),
Paul Ruet
(
IML) :
Logique permutative.

Résumé : Des travaux récents établissent un lien entre le nombre d'échanges d'une preuve de LL et la topologie du réseau associé, précisément le rang minimal des surfaces sur lesquelles le réseau peut être dessiné sans croisement. On peut calculer cette surface très simplement en séquentialisant le réseau dans un calcul qui est dérivé de celui de LL en enrichissant les séquents avec une structure appropriée (Métayer-Gaubert). L'objectif de l'exposé est de montrer que cette structure et ce calcul des séquents sont en fait (un fragment d')une instance des variétés-présentations (Andreoli). Le changement de point de vue donne lieu à un système qui satisfait les propriétés d'élimination des coupures et de focalisation, et arrive naturellement avec de nouvelles modalités qui gèrent la règle d'échange. LL et la logique cyclique peuvent se plonger dans ce système que nous appelons logique permutative, PL. Nous pensons que PL est un cadre naturel pour étudier et contraindre la complexité topologique des preuves, et donc l'usage de la règle d'échange.

jeudi 19 mai
----- à 14 h -----
salle de séminaire

Albert Burroni (
Preuves, Programmes et Systèmes, Paris 7) :
Traitement polygraphique de la bisimulation.

Résumé : Le contenu géométrique des structures du type "machines à calculer" (automates, grammaires, réseaux,...) est universellement décrit par des structures géométrico-combinatoires appelées polygraphes (généralisation en dimensions supérieures des graphes).
Par exemple, le concept de bisimulation des systèmes de transitions (qui sont des structures de dimension 1) est classiquement abordé en terme de graphes. Nous préciserons notre point de vue sur ce point, donc en dimension 1, puis, sur cette base, nous introduirons un concept de bisimulation en dimensions supérieures laquelle concerne des structures comme par exemple les machines de Turing ou les réseaux de Petri qui sont des structures de dimension 2. Nous montrerons certaines difficultés techniques rencontrées dans cette recherche.

mardi 26 avril
----- à 16 h -----
amphithéâtre

Romain Attal (
LPTM, Université de Cergy-Pontoise) :
La géométrie du Problème des Quatre Couleurs.

Résumé : Le Théorème des Quatre Couleurs affirme qu'il suffit de quatre couleurs pour colorier tout polyédre sphérique de sorte que les faces ayant une arête commune portent des couleurs distinctes. Les preuves connues (Appel & Haken, 1977 ; Robertson et al. , 1998) réduisent d'abord le problème à un nombre fini de configurations locales (réduction) puis font appel à un ordinateur pour démontrer qu'elles sont en fait coloriables (décharge) et en déduisent la coloriabilité dans tous les cas. Une autre voie possible (Penrose, Kauffman, Bar-Natan, ... ) consiste à linéariser le problème en exprimant le nombre de bons coloriages d'un polyèdre sphérique trivalent (hypothèse de stabilité non limitative) à l'aide du produit vectoriel dans R3. Penrose nous donne ainsi une formule très simple pour compter le nombre K de bons coloriages d'un tel polyèdre.
Le but de cet exposé est de donner une interprétation géométrique de la formule de Penrose en l'exprimant comme le résultat d'un transport parallèle. Pour cela, nous construisons au-dessus du polyèdre un espace fibré qui est le cadre naturel du problème de coloriage. L'opération de transport parallèle s'effectue en fait au-dessus de l'espace des chemins du graphe dual et est une succession d'opérations locales élémentaires sur des tenseurs de sl(2). Nous montrerons enfin comment le langage des catégories permet de mieux poser le Problème des Quatre Couleurs et pourrait nous amener à une preuve complète et sans machine du Théorème.

mardi 29 mars
----- à 14 h -----
amphithéâtre

Pierre Hyvernat (
IML) :
Systèmes d'interaction et lambda-calcul différentiel,
un modèle de "jeux synchrones".

Résumé : Les "systèmes d'interaction" peuvent servir à décrire de manière précise une interface régissant le fonctionnement d'un système concret. De manière plus abstraite, ils ressemblent aux notions de jeux "positionnels", où l'état courant est plus important que la séquence de coups.
Ces systèmes d'interaction peuvent interpréter toute la logique linéaire, en utilisant des opérations au caractère fortement synchrone. Les formules sont interprétées par des systèmes d'interaction ; et les preuves par des simulations entre les interfaces correspondantes.
Un des principes logique utilisé pour montrer la correction de ce modèle est fortement non-constructif. Je montrerais qu'on peut donner un modèle de la logique linéaire intuitionniste (plus précisément du lambda-calcul) en restant dans un cadre constructif. Cela permettrait, en théorie, d'obtenir des simulations concrètes à partir de preuves.
Enfin, je montrerais qu'on peut interpréter le lambda-calcul différentiel dans cette même catégorie...

mardi 1er mars
----- à 14 h -----
amphithéâtre

Thomas Streicher (
Technische Universität Darmstadt / invité IML) :
A Universal Model for Infinitary CPS Language in Locally Boolean Domains.

Résumé :
About 2 years ago Jim Laird has introduced a new kind of domains providing a fully abstract model for SPCF (i.e. PCF + catch) with non-recuperable errors. One can show that Laird domains provide a universal model for infinitary SPCF (i.e. with infinite terms). This has already been shown by J.Laird. But we give a simpler proof of this fact by showing that already type 1 over the natural numbers is universal for Laird domains.
SPCF hosts the recursive type $D \cong [D^\omega \to \Sigma]$ which provides a model for infinitary CPS target language (sort of an infinitary $\lambda$-calculus). It can be shown that every term of SPCF can be "realized'' by an object of $D$ that can be denoted by a term of the infinitary CPS language. From this it follows that every object of $D$ appears as denotation of an appropriate term of infinitary CPS, i.e.\ that $D$ is a universal model.
However, the model is not "fully complete'' because different infinite normal forms receive the same interpretation in D. This suggests that $\lambda$-calculus is not the optimal representation of sequential algorithms or, rather, that the model $D$ might give rise to an optimizing translation.
This is joint work with my student Tobias Löw.

mardi 22 février
----- à 14 h -----
amphithéâtre

Emmanuel Beffara (
PPS, Paris 7) :
Un modèle concurrent pour la logique linéaire.

Résumé :
Dans cet exposé, je développerai une réalisabilité sur un calcul concurrent à passage de noms dans le style du pi-calcul. À la base de l'édifice se trouvent des comportements définis par une notion paramétrable de test (divergence, must-testing...), sur lesquels on définit ensuite des connecteurs inspirés de logiques spatiales (conjonction séparante, implication spatiale) et temporelles (modalités à la Hennessy-Milner). De ces connecteurs, on déduit d'une part un modèle concurrent de la logique linéaire, et d'autre part un système de types pour les processus sous-jacents, qui établit une correspondance à la Curry-Howard entre concurrence et logique linéaire. Cette correspondance a le bon goût de factoriser les traductions standard du lambda-calcul dans le pi-calcul par des traductions des logiques intuitionniste et classique dans la logique linéaire, ce qui formalise des intuitions concurrentes sur le contenu calculatoire des diverses logiques sus-nommées.

mardi 1er février
----- à 10 h -----
amphithéâtre

Pierre Boudes (
IML) :
Expériences et arbres de Böhm abstraits.

Résumé :
Les arbres de Böhm abstraits de Curien, ABTs, fournissent une représentation fidèle des réseaux de preuves sans coupure du fragment multiplicatif exponentiel de la logique linéaire polarisée, MELLpol (et cette représentation s'étend facilement à tout LLpol). On obtient alors des ABTs typés que vous reconnaîtrez aussi comme étant des stratégies innocentes, ou des desseins (de la ludique) avec exponentielles. La notion d'expérience dans les réseaux bénéficie aussi de cette traduction dans les ABTs. Pour cela on introduit une notion de sous arbre épais d'un arbre. Un sous-arbre épais d'un arbre T est la donnée d'un arbre E et d'un morphisme d'arbre de E dans T (un morphisme d'arbre envoie la racine sur la racine et la précédence sur la précédence). Une expérience dans un ABT P de type A est alors un sous-arbre épais de P et son résultat est un sous-arbre épais de A. Le calcul de la sémantique relationnelle des réseaux peut alors être effectué dans les ABTs.
Je présenterais les notions d'arbre épais et d'arbre de Böhm abstrait et je montrerais le rapport avec les réseaux MELLpol, ainsi qu'avec leurs interprétations dans les jeux. En fonction du temps, je discuterais aussi la conjecture de l'injectivité du modèle relationnelle dans ce cadre et je parlerais un peu de logique linéaire indexée.

mardi 25 janvier
----- à 10 h -----
amphithéâtre

Marcelo Fiore (
Christ's College, University of Cambridge) :
Generalised Species of Structures.

Résumé :
This piece of work is part of my research interest in approaching computation structure from a combinatorial perspective; in particular, in regarding data type structure as combinatorial structure, and vice versa. This view has given interesting connections between various areas of theoretical computer science and mathematics, and in this talk I will present one such concerning topics in category theory, combinatorics, logic, and models of computation. Specifically, I will motivate and introduce a generalisation of Joyal's notion of species of structures, and develop the associated combinatorial calculus. As I will show, these generalised species have a rich mathematical structure (akin to models of Girard's linear logic) that can be described purely within Lawvere's generalised logic. Indeed, I will present and treat the cartesian closed structure, the linear structure, the differential structure, etc. of generalised species axiomatically in this mathematical framework. As an upshot, I will observe that the setting allows for computational interpretations of the lambda calculus (both typed and untyped), the differential lambda calculus of Ehrhard and Regnier, etc...

EL, le 25 novembre 2005