Résumé : Light linear logic and its affine variant, known as light affine logic, are logical systems which precisely capture the polynomial time complexity. In particular, it is known that proofs of these systems are polytime *weakly* normalizable. In this talk, we consider a proper term calculus for light affine logic and show its polytime *strong* normalizability, and then discuss its extension to the polynomial space complexity. We first introduce light affine lambda calculus (lambda-LA), a simple modification of the standard lambda calculus, which can be seen as an untyped version of intuitionistic light affine logic. Proofs of the latter can be represented as terms of lambda-LA. Then we show the polytime *strong* normalization theorem: whatever reduction strategy we take, we can normalize a given term of lambda-LA in polynomial time. We then introduce its extension, polyspace affine lambda calculus, which precisely capture the polynomial space complexity. Our idea essentially relies on the notion of slice. Recall that the crucial condition in the proof syntax of light logics is that we can build a !-box around a proof t only when t has at most one assumption (free variable). We relax this condition so that, roughly speaking, we can also build a !-box when each *slice* of t has at most one assumption.

Mardi 4 Décembre 2001
à 10h 15
Amphithéâtre
Claudia Faggian (IML) :
Ludics, interactive observability, games.

Mardi 13 Novembre 2001
à 10h 15
Amphithéâtre
Marie-Renée Fleury-Donnadieu (IML) :
1er Ordre en Ludique.

Résumé: Les résultats présentés aujourd'hui ont fait l'objet d'un travail en commun avec Myriam QUATRINI (IML). Ils se placent dans le cadre de la théorie de la démonstration dite "La Ludique" ; cette théorie a été développée par J-Y. GIRARD [1] Nous étudions une interprétation du calcul des séquents de la logique linéaire MALL2 auquel on rajoute les quantificateurs du 1er ordre. La partie principale de l'exposé sera consacrée à la propriété d'uniformité qui s'avère nécessaire dés que l'on s'intéresse à la généralisation du "full completeness theorem" obtenu pour MALL2 dans [1].
[1] J-Y. GIRARD Locus Solum , MSCS 2001.

Mardi 23 Octobre à 14h
Salle de Séminaire
Christophe Raffalli (Université de Savoie) :
Un système de type pour l'extraction ET la preuve de programme.

Résumé : La logique linéaire light est une contribution de la théorie de la démonstration à la caractérisation du temps polynomial. Elle a été introduite par Jean-Yves Girard dans [1] et une variante affine a été proposée par Andrea Asperti ([2]). Dans cet exposé je présenterai ces deux systèmes ainsi que les théorèmes de représentation et de normalisation en temps polynomial. Si le temps le permet nous discuterons de l'utilisation de ces logiques comme systèmes de types et nous les comparerons à d'autres systèmes de types pour la complexité.
[1] J.-Y. Girard. Light linear logic Information and Computation 143, 1998.
[2] A. Asperti. Light affine logic, LICS'98.

Lundi 25 Juin à 16h
Philip Scott (Université d'Ottawa-Invité IML)
Bounded Linear Logic: Realizability Models.

Résumé : Bounded Linear Logic (BLL) (Girard, Scedrov, Scott, TCS, 1992) was an early attempt to provide an intrinsic notion of ptime computation within a linear logical system. While it has some disadvantages compared to recent logical systems (e.g. LLL, SLL), it has its own merits: from a computer science viewpoint, BLL determines a natural polymorphically-typed functional language in which bounded storage can represent bounded calls to memory. The main theorem in the original paper was that the numerical functions representable (by proofs) in the system are exactly the ptime functions. We give a new model-theoretic proof of the main direction ("representable implies ptime"), using realizability models. At the same time, the model suggests other rules and principles that may be added consistently to BLL, and are closer in spirit to some of the more recent systems above. This is joint work with Martin Hofmann.

Lundi 25 Juin à 10h
Jean-Yves Girard (CNRS- IML)
La structure locative des exponentielles.

19 Juin à 14h30
M. Hyland (Univ.Cambridge)
Interaction of Strategies by Composition of Interleavings.

Résumé : Proofs and programmes can be modelled in categories where the maps or morphisms are strategies in some kind of game. Composition is obtained by nteracting the strategies in a way which reflects the Cut rule in logic, and parallel composition plus hiding for processes. The associativity of the composition, that is, the existence of the category itself, is a delicate matter. Proofs of what seems obvious seem tiresome, and are often skipped in the literature. In fact the issue is not straightforward: if one considers together games in which Opponent starts (negative games) and games in which Player starts (positive games), then on the natural interpretation composition is not associative. This is the "Blass Problem". We introduce a general technology for proving associativity of composition. In outline the idea is as follows. Start from the (appealing denotational) view that strategies correspond to the collections of plays according to them. (Applications of the technology may require a permissive reading: these plays could be against a wild opponent.) Now the plays corresponding to a strategy in a linear function space can be regarded as interleavings of plays in the two components. (Again the notion of play in a component needs flexible interpretation: as illustrated by the simple case of Conway games, one may want to consider potential rather than real plays.) We show that we can regard the interleavings of component plays p and q as the maps u: p \to q in something like a category of relations. Then a strategy phi is just given by a collection of such maps. In these terms composition is defined simply by \[ \psi\, . \, \phi = \{ \, v.u \, | \, v \in \psi \mbox{ {\rm and} } u \in \phi \, \} \] where implicitly {\rm dom}( v) = {\rm cod}(u). Associativity of composition is now manifest. The most obvious kinds of games used in semantics are essentially sequential: as such they model intuitionistic linear logic, and/or (the more refined) polarised linear logic. The idea of `abstract games' readily leads to models of classical linear logic, and may be regarded as providing some abstract notion of concurrent computation. The proof technique described leads naturally to a more concrete style of concurrent game: there is simply no need for plays to be linearly ordered. The idea of such concurrent games can be illustrated by consideration of the "Blass problem".

Mardi 12 Juin à 14h
Salle de Séminaire
Benjamin Werner
(INRIA)
Cinq-cent millions de petits lemmes (le théorème des 4 couleurs en Coq)

Résumé : Ici je parlerai de la tentative courante de formaliser en Coq la preuve complète du théorème des 4 couleurs. Cette preuve très particulière est aussi une bonne occasion d'évoquer l'interaction entre déduction logique et calcul. Plus généralement, elle permet de souligner de manière très concrète que l'avènement de la vérification mécanique change le regard que nous portons sur les formalismes logiques.

Mardi 5 Juin à 14h
Salle de Séminaire
Kohei Honda
(Queen Mary and Westfield College, London)
Sequentiality and the Pi-Calculus

Résumé: ici This talk is about syntax, a typed syntax which captures diverse classes of programming languages and computational behaviours, of which I concentrate on sequential functional behaviour.

Résumé : La plupart des circuits électroniques numériques sont "synchrones", c'est-à-dire qu'ils changent d'état après chaque top d'un signal d'horloge, global et périodique. Le modèle de calcul peut se passer de prendre en compte le parallélisme, alors même que ces circuits comportent des millions de portes logiques, et que les temps de propagation des signaux au sein d'une puce de Silicium peuvent être bien supérieurs à la durée de la période d'horloge. Dans ces circuits, la gestion de la synchronisation par l'horloge représente un coût de plus en plus important, tant en terme de surface de Silicium, qu'en terme de consommation électrique, ou en terme d'effort de développement.
Les circuits "asynchrones" sont définis par l'absence d'horloge. Ils constituent une classe plus générale de circuits, pour laquelle la prise en compte du parallélisme est indispensable. Plusieurs méthodes sont développées, qui permettent de concevoir des circuits de complexité élevée. Il est important de pouvoir, comme dans le cas synchrone, bien séparer la mise au point de la fonction logique d'une part, de son implémentation physique d'autre part. Une façon de le faire est d'essayer de se limiter à la classe des circuits DI (delay-insensitive), pour lesquels le résultat du calcul est indépendant des temps de propagation des messages. Peut-on définir un jeu de circuits DI primitifs et une loi de composition qui conserve cette propriété DI ?
En introduction à ce domaine, nous commenterons quelques publications qui nous semblent représentatives des questions abordées par cette communauté.

Mardi 15 Mai à 14h
Salle de Séminaire
Didier Remy
(INRIA)
Une généralisation des exceptions et des opérateurs de contrôle.

Résumé : (Travail en collaboration avec Jon Riecke et Carl Gunter)
Les opérateurs de contrôle dérivés du "call/cc" du langage scheme ont eu un grand succès à la fin des années 80 conduisant à un foisonnement de nouvelles espèces. Son apparition dans le langage SML au début des années 90 a soulevé de sérieux problèmes de typage. En fait, le typage dérivé de la traduction par double négation n'est pas vraiment satisfaisant, car il repose sur une vue fermée du monde, ne permet qu'un résultat de correction faible, et oblige ainsi le toplevel à quelques acrobaties mystérieuses. Dans c'est exposé je présenterai des travaux menés en 95 pour résoudre ce problème de typage. Je montrerai comment nous avons été amenés à introduire une nouvelle opération "cupto" (call up to) obligeant la capture de la continuation à faire référence à un point précis du calcul (prompt) introduit explicitement par le programmeur. Nous donnerons des règles de typage pour cette construction qui permettent un résultat de correction forte (préservation du typage au cours de la réduction). Nous montrerons également que cette construction généralise la plupart des constructions proposées jusqu'alors (1995) y compris le mécanisme d'exception de ML. Nous verrons aussi sur des exemples concrets que le cupto est un opérateur plus facile à manipuler que ses cousins et parents. Mais la manipulation explicite des continuations par le programmeur reste délicate, même avec le "cupto", et est finalement réservée à des applications très spécifiques.

Résumé : En 1968, E. W. Dijkstra proposa une "image" géométrique de threads communiquant à travers une mémoire partagée (les "progress graphs"). L'idée est toute simple: on associe à chaque processus une coordonnée d'un espace euclidien (son "temps local d'exécution"). Les conditions d'exclusion mutuelle associées à des locations en mémoire partagée délimitent des zones "interdites", dans lesquelles ne peut passer aucun chemin d'exécution. Topologiquement, les espaces à étudier sont des espaces topologiques muni d'un ordre partiel fermé, et les chemins "intéressants" sont les chemins continus, croissants en chaque coordonnée (on ne peut inverser les temps locaux). Dès lors, on peut tenter de se poser des questions sur les propriétés de ces systèmes parallèles en termes topologiques et géométriques. Il se trouve que les points morts, les états inatteignables, les "ordonnancements essentiels" etc. sont en fait des propriétés invariantes par certaines déformations continues, ou homotopies. La question essentielle est alors, quelle est la topologie algébrique "dirigée" qui nous renseignera efficacement sur ces propriétés? Considérer des invariants (comme des théories homologiques par exemple) pour cette théorie de la déformation orientée revient à faire des abstractions du système; un équivalent du théorème de Van Kampen permettrait de parler de "compositionalité"; utiliser des rétracts de ces formes reviendrait à faire de la "réduction de l'espace d'états" etc. thèmes chers à l'analyse statique. En fait, beaucoup d'autres concepts sont d'intérêt, et pas seulement pour l'analyse statique de programmes parallèles; citons des résultats concernant la théorie des domaines, quelques considérations logiques (en collaboration avec mon frère, Jean Goubault-Larrecq) et sur la reécriture, la correction de protocoles de bases de données (Carson, Reynolds, Lipsky, Papadimitriou, J. Gunawardena etc.), les protocoles tolérants aux pannes (Herlihy, Rajsbaum, Shavit etc.). J'essaierai dans cet exposé de donner une idée des formalisations récentes de ces problèmes. En effet le modèles des "progress graphs" est trop particulier pour être vraiment utile de façon générale, il faut passer à des espaces localement partiellement orientés (collaboration avec Martin Raussen et Lisbeth Fajstrup), ou de façon combinatoire à des ensembles cubiques généraux, ou à des omega-catégories (Vaughan Pratt, Philippe Gaucher). Je passerai en revue quelques résultats importants et quelques directions de recherche actuelles.

Mardi 16 Janvier
le matin à 10 h (amphi)
Titre à préciser.
l'aprés midi (salle séminaire)
Titre à préciser.