Institut de Mathématiques de Luminy

SÉMINAIRES 2002
Logique de la Programmation (LDP)

Organisatrice :

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

Mardi 10 décembre

----- à 14h30 -----
Amphithéâtre
Jean-Yves Girard (IML) :
Entre Logique et Quantique .

Résumé :
J'interprète (1) le fragment perfectif (2) de la logique (i.e., MALL) dans les espaces cohérents quantiques (3) (ECQ), version "non-commutative" des espaces cohérents. C'est simple (c'est de la géométrie hermitienne de dimension finie) et ça décoiffe.
a) La \eta-expansion correspond à la réduction du paquet d'onde, le phénomène quantique de base (4). Plus généralement, l'utilisation exclusive d'hermitiens positifs correspond à une version \eta-expansée de la logique.
b) L'identité \lambda x x existe aussi, mais elle ne correspond pas à un opérateur positif. Le phénomène est sensible dès la dimension 2 (spin 1/2).
c) L'opposition positif/négatif correspond à l'opposition fonction d'onde/appareil de mesure.
d) En dimension 2, il existe un continuum d'ECQ, (les booléens suivant telle ou telle base), qui sont tous sous-types de qBool, les booléens quantiques.
e) Il faut évidemment compléter la partie perfective (quantificateurs) et ajouter les opérations imperfectives (exponentielles), mais ça demande le passage en dimension infinie, avec infiniment de problèmes.... (5)
Notes :
1) A l'origine, les travaux sur la logique linéaire (espaces de Banach cohérents) ; plus récemment la notion de polarité de la ludique. Et, last but not least, le langage de programmation quantique de Selinger.
2) Les langues slaves dédoublent tous les verbes en perfectif (ex : skazat', parler dans un contexte précis) et imperfectif (ex : gavarit', savoir parler russe), qui expriment une nuance de la même nature que passé simple/imparfait, mais en plus radical.
3) La logique quantique se donnait pour but d'"expliquer" la mécanique quantique au moyen d'un paradigme logique réaliste syntaxe/sémantique, a priori antagoniste à la mécanique quantique, elle-même violemment non-réaliste. Au contraire, j'interprète la logique dans le quantique. Ce qui ne veut pas dire que cette interprétation n'aide pas à comprendre le quantique... nous le verrons au cours de l'exposé.
4) Qui aurait cru qu'un sujet aussi rebattu et académique que "\eta" (si tu ne sais plus quoi faire, reprends ton article avec \eta !) cachât un scorpion de cette taille.
5) L'avantage de l'état actuel, très incomplet, c'est que ça reste simple... et irréfragable.

----- à 10h15 -----
Amphithéâtre
Luigi Santocanale (LaBRI - Université Bordeaux 1) :
Un théorème d'interpolation dans les théories des preuves circulaires.

Résumé :
n \mu -calcul est une logique propositionnelle avec des opérateurs de point fixe \mu et \nu . Par exemple, étant donnée une formule propositionelle t(x) dont l'interprétation est une fonction monotone f: L \rightarrow L sur un treillis complet, on ajoute deux nouvelles formules \mu_{x}.t(x) et \nu_{x}.t(x) pour dénoter les plus petit point fixe et les plus grand point fixe de f , respectivement.
Les opérateurs \mu et \nu sont semblables à des quantificateurs, et on définit des classes \Sigma_{n} et \Pi_{n} comme il suit: \Sigma_{0} = \Pi_{0} est la classe des tous les termes sans application des opérateurs de point fixe; \Sigma_{n+1} est la clôture de \Sigma_{n} et \Pi_{n} sous la substitution et l'opérateur \mu ; \Pi_{n+1} est la clôture de \Sigma_{n} et \Pi_{n} sous la substitution et l'opérateur \nu .
Dans cet exposé je vais montrer comment on peut utiliser des outils de la théorie des preuves pour montrer le fait suivant : soient t \in \Pi_{n + 1} et s \in \Sigma_{n + 1} deux \mu -termes dans la signature des treillis \langle \top,\land,\bot,\vee\rangle ; si pour toute interprétation dans un treillis complet on a \eval{t} \leq \eval{s} , alors ils existe un \mu -terme r tel que: 1) pour toute interprétation \eval{t} \leq \eval{r} et \eval{r} \leq \eval{s} , 2) il appartient à la clôture de \Sigma_{n} et \Pi_{n} sous la seule opération de substitution.
Les preuves que nous considérons sont en effet des stratégies gagnantes dans des jeux avec des boucles ; pour cette raison elles aussi peuvent avoir des boucles.

Lundi 28 octobre

----- de 16h à 18h -----
Amphithéâtre
Gérard Meunier :
Implantation parallèle des réseaux d'interaction.

Mercredi 26 juin

----- à 14h30 -----
Salle de séminaires
Ian Mackie (Lab.Informatique École Polytechnique) :
Extanding Interaction Nets.

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

----- à 15h30 -----
Salle de séminaires
Denis Bechet (Université Paris 13 & INRIA) :
Interfaces de taille polynomiale pour les modules de MLL.

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

Mardi 25 juin

----- à 10h15 -----
Amphi
Jerzy Tiuryn (University of Warsaw) :
Substructural Logic and Partial Correctness.

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

Mardi 18 juin

----- à 10h15 -----
Salle de séminaires
Jean-Yves Girard (IML) :
GoI revisited.

Résumé : Work in progress, possible connections with next talk.

----- à 14h15 -----
Salle de séminaires
Peter Selinger (University of Ottawa) :
Towards a quantum programming language.

Résumé : The field of quantum computation suffers from a lack of syntax. In the absence of a convenient programming language, algorithms are frequently expressed in terms of circuits or Turing machines. Neither approach particularly encourages structured programming or abstractions such as data types. In this talk, I describe the syntax and semantics of a simple quantum programming language. The semantics is interesting because it combines notions from geometry of interaction, linear algebra, category theory, and complete partial orders.

Lundi 17 juin

----- à 10h15 -----
Salle de séminaires
(Groupe de Travail)
Peter Selinger (University of Ottawa) :
Basics of Quantum Computing.

Mardi 19 mars

----- à 10h15 -----
Salle de séminaires
Rick Blute (University of Ottawa and IML guest) :
An (informal) introduction to Quillen model categories.

Résumé : Quillen model categories are an attempt to define the notion of axiomatic homotopy theory. From this point of view, the crucial aspect of homotopy theory is the passage from the category TOP of topological spaces to the category Ho(TOP) of homotopy equivalence classes of maps. Of special interest are the weak equivalences. These are maps which become isomorphisms in the passage to Ho(TOP). A Quillen model category is a category C with a specified class of morphisms, the weak equivalences, which has sufficient structure to define a homotopy category Ho(C) in which the weak equivalences become isomorphisms. From the straightforward axioms of the definition, one can derive a number of remarkable consequences. I will conclude by speculating on some possible applications to concurrency theory.

Mardi 12 mars

----- à 11h00 -----
Amphithéâtre
Pierre-Louis Curien :
Abstract Boehm trees.
----- à 14h30 -----
Amphithéâtre
Olivier Danvy :
TBA.
----- à 16h00 -----
Amphithéâtre
Vincent Danos :
Communication Models & Biological Pathways
.

Lundi 11 mars

----- à 14h30 -----
Amphithéâtre
Jean-Louis Krivine :
TBA.
----- à 16h00 -----
Amphithéâtre
Martin Hyland :
Embedding Theorems and Conservative Extensions.

Mardi 22 janvier
----- à 10h30 -----
Amphithéâtre
Rike Blute ( University of Ottawa and IML guest) :
Nuclear Ideals and Formal Distributions.
-----à 14h30
-----
Salle de séminaires
Jean marc Andreoli ( Xerox Research Centre Europe +IML) :
Construction de réseaux focalisés.

Résumé : Cet exposé relate mon travail récent sur les réseaux focalisés. Ceux-ci exploitent de façon essentielle la focalisation non seulement sur les formules composées, mais surtout sur les formules atomiques. Un critère de correction, adapté du critère Danos-Régnier classique, est proposé, pour les réseaux focalisés éventuellement incomplets, ainsi qu'une démonstration de la validité de ce critère (je ne sais pas si elle est originale). De plus, une "compilation" permettant d'optimiser la vérification du réseau est également proposée. Ce travail permet une nouvelle approche du paradigme de programmation par construction de preuves.

Mardi 8 janvier
----- à 10h15 -----
Christophe Gaubert (IML) :

Structures de preuves en deux dimensions et règle d'échange.

Résumé : Dans son article [1] , Métayer transforme les réseaux multiplicatifs en surfaces orientables à bord. Il explore le lien entre nombre d'échanges d'une séquentialisation et complexité topologique. Le théorème qu'il obtient parle en fait d'une règle d'échange particulière (transposition par blocs). On complète son approche en montrant que la complexité topologique ne fournit pas d'information dans les autres cas possibles (permutation arbitraire, majoration du nombre d'échanges). Puis on montre que la surface associée à un réseau est en fait la surface de complexité minimale sur laquelle on peut dessiner le réseau, en respectant l'orientation locale et sans croisement.

[1] "Implicit exchange in multiplicative proofnets", F. Métayer, MSCS, 11: 261-272, 2001

EL, le 19 décembre 2002.