LOGIQUE DE LA PROGRAMMATION

Séminaires 2003-2004

Organisatrice : Marie-Renée Fleury-Donnadieu (téléphone : 04 91 26 96 38). 
Horaire : en règle générale le mardi. 
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.


Retour à la page d'accueil du Séminaire

à 10h    Amphithéatre Herbrand (1er étage)


Pierre HYVERNAT (IML )

Transformateurs de prédicats : encore un modèle dénotationnel de la logique linéaire     

Résumé : Je construit un modèle dénotationnel de la logique linéaire (avec exponentielles) en utilisant des « transformateurs de prédicats » (opérateurs sur les parties d'un ensemble). Ces transformateurs de prédicats sont utilisés en informatique pour donner une sémantiques aux spécifications et aux programmes séquentiels ; et les opérations logiques correspondent à des opérations sur les spécifications / programmes.

Les preuves sont interprétés comme dans le modèle relationnel, et sémantiquement parlant, sont des « propriétés des sûreté » pour la spécification correspondant à la formule prouvée.

Je donnerais la construction de ce modèle, ainsi que les problèmes rencontrés ; et je mentionnerais brièvement comment on peut l'étendre au second ordre, et/ou comment on peut en faire un modèle du lambda calculs différentiel de Thomas et Laurent...



à 10h    Amphithéatre Herbrand (1er étage)


Robin COCKETT   (University of Calgary )

The logic of polarized cut and its semantics     

Résumé : Starting with the interpretation of games as (categorical modules) we build up to the presentation of the logic of polarized cut and its polarized polycategorical semantics. We show how from such a polarized semantics one can "depolarize" to obtain a classical semantics for linear logic. The issue of which constructs survive depolarization is of some interest. I shall discuss how the multiplicative and additive structure survives the process.

The fact that the additives can be made to survive is a bit of a surprise as in the original Abramsky-Jagadeesan work the fact that the additives did not survive was a central feature.

Finally it is worth noting that nowhere need one assume that the multiplicative structure is commutative. Thus, these methods of construction can be used to generate non-commutative models of linear logic with a game theoretic flavor.

This is joint work with Robert Seely. A draft of the paper available on request.



à 14h     salle de séminaires (3ème étage)


Yves LAFONT (IML, Institut de Maths de Luminy )

Théorie homotopique des calculs : le Programme de Minneapolis     

Résumé : 1. L'égalité algèbrique est illusoire : il y a seulement des calculs qui relient des expressions bien distinctes.
2. Principe de cohérence : deux calculs qui prouvent la même "égalité" doivent être considérés comme "égaux".
3. Cette égalité entre calculs est elle-même illusoire : on la remplace par des calculs entre calculs.
4. On continue ainsi ad infinitum.

Ce processus n'est pas un serpent qui se mange la queue. On peut lui associer un contenu mathématique précis : c'est une "résolution" de Métayer. Cette notion s'exprime elle-même en termes de "polygraphes" de Burroni ou de "computades" de Street. Nous pensons qu'elle permet d'unifier et de généraliser des approches qui sont visiblement apparentées comme les théorèmes de cohérence en théorie des catégories (Mac Lane & autres), les invariants homologiques et homotopiques de la réécriture (Squier & autres), ou l'homologie des groupes Gaussiens (Dehornoy & Lafont). Dans cet esprit, nous avons dressé une liste d'une quinzaine de conjectures ou de directions de recherche (Programme de Minneapolis).

Travail en commun avec François Métayer.



  • Lundi 21 Juin 2004

à 14h     Amphithéatre Herbrand (1er étage)


Alexandre MIQUEL     (PPS [Preuves, Programmes et Systèmes] - Paris 7)

Un théorème de normalisation forte pour IZF     

Résumé : Dans cet exposé, je montrerai comment le paradigme (dû à Aczel) consistant à interpréter les ensembles par des graphes pointés et l'égalité extensionnelle par la bissimilarité permet de construire un modèle de normalisation forte de la théorie des ensembles intuitionniste (IZF), c'est-à-dire un modèle de réalisabilité dans lequel toutes les formules prouvables de IZF sont réalisées par des lambda-termes fortement normalisables. En particulier, cette forme de réalisabilité me permet d'affiner un résultat classique de Myhill et Friedman, en montrant que toute fonction numérique dont l'existence est prouvable dans IZF est calculable par un lambda-terme fortement normalisable de type Nat -> Nat. Enfin, je montrerai comment il est possible de construire concrètement des lambda-termes (assez complexes) qui réalisent chacun des axiomes de IZF, en passant par un système de types ad hoc suffisamment proche du système de types de l'assistant à la démonstration Coq pour pouvoir être simulé aisément dans ce dernier.



  • Mardi 25 Mai 2004
     

à 10 h.     Amphithéatre Herbrand (1er étage)


Harry MAIRSON      (Brandeis University & Invité IML)     

Linearity, type inference, and normalization: from impotency to idempotency.

Résumé :Abstract : In this talk, I want to contrast the computational complexity of type inference, which is a fairly canonical approximate static analysis done by compilers, with related run-time bounds on the cost of normalization. The original motivation was to understand some linear logic foundations of type inference from a complexity perspective; a more recent motivation has been to analyze the intersection type system "System I" proposed in the Church compiler project at Boston University. Type inference for simply-typed lambda calculus is PTIME-complete, but in contrast, deciding equivalence of two terms is nonelementary (Statman's theorem). The PTIME result can be derived straightforwardly from circuits coded as linear terms, with a crude quasi-linear hacking of contraction and deriliction for Booleans, while the Statman result depends crucially on nonlinear terms. (A non-affine variant on this very simple construction gives the PTIME-completeness of normalization for MLL and a multiplicative LLL, which we will discuss briefly.) These results extend naturally to ML, where we get EXPTIME-completeness for type inference, and a turbo-nonelementary Statman theorem. The results do not further extend to System I because in the latter, the intersection operator is not idempotent, a decision made to facilitate control flow program analysis, which reduces essentially to an American recapitulation of the geometry of interaction. As a consequence, however, the intersection-free fragment of System I degrades to the linear lambda calculus, and the complexity of normalization collapses to that of of type inference; adding idempotence recovers an expressive power commensurate with ELL, restoring the relationship seen between type inference and normalization for simple types and ML. We learn two things: first, that the static analysis of type inference, in the case of System I, involves no approximation, but is merely---and uninterestingly---the computation of normal forms. Second, that the complexity of type inference for such systems depends on the largely technical, and peculiar facility in these calculi to polymorphically iterate linear functions with different domains and ranges.
 
 

à 14h15     Salle de Séminaires (3ème étage)


Jean-Yves GIRARD     (CNRS - Institut de Maths de Luminy, Marseille)

Géométrie de l'Interaction 4



2h30 le matin et 2h30 l'après-midi.     Amphithéatre Herbrand (1er étage)


Jean-Louis KRIVINE     (PPS [Preuves, Programmes et Systèmes] - Paris)

Réalisabilité en analyse classique et dans ZF.     

Contenu du cours : La correspondance de Curry-Howard transforme les preuves en programmes, mais seulement pour les preuves en logique pure. Or, les preuves mathématiques utilisent un système d'axiomes (habituellement l'analyse ou la théorie des ensembles) qu'il faut donc interpréter par des programmes convenables, si on veut étendre cette correspondance aux mathématiques usuelles.
 
  On donne, dans ce cours, une méthode pour y parvenir. Les programmes obtenus sont écrits dans un lambda-calcul, étendu avec de nouvelles instructions, mais où l'exécution est déterministe (essentiellement, la réduction de tête faible). Les axiomes les plus difficiles à interpréter sont l'axiome d'extensionnalité et l'axiome du choix dépendant. L'axiome du choix complet est, pour le moment, un problème ouvert.



  • Mardi 18 Mai 2004

à 10h     Amphithéatre Herbrand (1er étage)


Antoine RAUZY     (CNRS - IML )

Peut-on faire confiance aux modèles booléens d'analyse du risque ?     

Résumé Les analyses du risque dans les installations industrielles sensibles (centrales nucléaires, usines chimiques, avion, ...) se font principalement en utilisant des formalismes booléens (arbres de défaillance, arbres d'événements).
Le traitement de ces modèles posent de nombreuses questions méthodologiques (adéquation des modèles à la réalité) et algorithmiques (les problèmes à résoudre étant tous fortement combinatoires). Le but de l'exposé est double: d'une part, je ferais une présentation générale de ces méthodes d'analyse du risque, d'autre part je vous parlerais de quelques résulats pratiques inquiétants que j'ai obtenu récemment en reprenant une étude probabiliste de sûreté sur une centrale nucléaire japonaise.



  • Mardi 16 Mars 2004

à 14 h, Salle de Séminaire (3ème étage)


Emmanuel BEFFARA     (P.P.S. [Preuves, Programmes et Systèmes] - Paris)

Réseaux de preuve et calcul de processus.     

Résumé : On introduit une traduction des réseaux de preuve avec changements de polarité explicites vers le calcul de fusion de Parrow et Victor (cousin du pi-calcul). Cette traduction, polarisée et typée, se fonde sur une décomposition des connecteurs. Les réductions qui ont lieu dans les traductions font apparaître naturellement des connecteurs multiples et autres éléments du folklore linéaire. On en déduit ensuite une traduction épurée qui interprète une preuve comme un processus dans lequel les actions (c'est-à-dire les communications) correspondent exactement aux changements de polarité, le reste n'étant que règles structurelles.



  • Exposé reporté

à 10h, Amphithéatre Herbrand


Jean-Yves GIRARD     (CNRS-Institut de Maths de Luminy, Marseille)

Géométrie de l'Interaction IV.     

Résumé :



  • Mardi 3 Février 2004

à 14h, Salle de séminaires (3ème étage)


Yves GUIRAUD     (Université Montpellier)

Terminaison et réécriture d'opérateurs.     

Résumé : Suivant les idées d'Albert Burroni, un cadre "diagrammatique" fournit une interprétation naturelle de plusieurs sortes de systèmes de réécriture classiques, parmi lesquels les réseaux de Pétri, les termes et le lambda-calcul. Dans les deux derniers cas, on peut même relever les chemins de réécriture, en explicitant les opérations de gestion des ressources et de substitution des variables liées. Cependant, les "termes" de cette réécriture d'opérateurs nécessitent des techniques nouvelles, notamment pour les preuves de terminaison : nous en verrons une qui fonctionne dans de nombreux cas.
 
 

  • Lundi 8 Décembre

à 14h, Salle de séminaires (3ème étage) (à préciser)


Jean-Louis KRIVINE     (Université Paris VII - PPS)

L'axiome du choix dépendant et l'horloge.     

Résumé : Une bonne part des preuves mathématiques se formalise bien en analyse, c'est-à-dire en logique classique du second ordre avec axiome du choix dépendant. Pour transformer ces preuves en programmes, il reste à décrire l'instruction associée à l'axiome du choix dépendant. Une solution simple consiste à utiliser, pour cela, l'horloge du système informatique.
 
 

  • Mardi 14 Octobre

à 10 h, Amphithéatre Herbrand (1er étage)


Jean-Yves GIRARD     (CNRS - Institut de Maths de Luminy, Marseille)

Espaces Cohérents Quantiques (suite)

Résumé : L'article "LLcup.ps.gz" est disponible : ICI
 
 

  • Mardi 7 Octobre

  • à 10h, Amphithéatre Herbrand (1er étage)


Pierre HYVERNAT     (Institut de Maths de Luminy, Marseille)

Une jolie catégorie de transformeurs de prédicat.     

Résumé : Un transformeur de prédicat de A dans B est une fonction des sous-ensembles de A dans les sous-ensembles de B. Les transformeurs de prédicat monotones sont importants en informatique théorique. Il ont permis de donner une sémantique élégante à des langages de programmation. (Calcul wp de Dijkstra.)
Je présenterais une catégorie dont les objets sont des transformeurs de prédicat, et les morphismes des "simulations".
Cette catégorie a toutes les constructions nécessaires pour en faire une catégorie linéaire : * produit et coproduit (qui coïncident !) ; * symétrique monoidale fermée (un tenseur et un par) ; * auto-dual (négation) ; * "*"-autonome.
Cette catégorie admet en plus deux autres tenseurs intéressants.

On peut présenter les transformeurs de prédicats comme des "jeux" (appelés "systèmes d'interaction"). J'expliquerais pourquoi et comment.

Références :
"A nice category of (monotonic) predicate transformers": http://iml.univ-mrs.fr/~hyvernat/Files/PT.ps.gz

"A mathematical study of interaction systems": http://iml.univ-mrs.fr/~hyvernat/Files/phd_chalmers.ps.gz
 
 

  • à 14h 15 , Salle de Séminaires (3ème étage)


Jean-Yves GIRARD     (CNRS - Institut de Maths de Luminy, Marseille)

Espaces Cohérents Quantiques

Résumé :
 
 

  • Mardi 16 Septembre,

à 10 h, Amphithéatre Herbrand (1er étage)


Kazushige TERUI     (National Institute of Informatics, Tokyo, Japan)

On the computational complexity of cut-elimination in linear logic

Résumé : Given two proofs in a logical system with a confluent cut-elimination procedure, the cut-elimination problem (CEP) is to decide whether these proofs reduce to the same normal form. This decision problem has been shown to be PTIME-complete for Multiplicative Linear Logic (Mairson 2003). The latter result depends upon a restricted simulation of weakening and contraction for boolean values in MLL; in this talk, we analyze how and when this technique can be generalized to other MLL formulas, and then consider CEP for other subsystems of Linear Logic.

We also show that while additives play the role of nondeterminism in cut-elimination, they are not needed to express deterministic PTIME computation. As a consequence, affine features are irrelevant to expressing PTIME computation. In particular, Multiplicative Light Linear Logic (MLLL) and Multiplicative Soft Linear Logic (MSLL) capture PTIME even without additives nor unrestricted weakening.

We establish hierarchical results on the cut-elimination problem for MLL (PTIME-complete), MALL (coNP-complete), MSLL (EXPTIME-complete), and for MLLL (2EXPTIME-complete).

This is a joint work with Harry Mairson.
 
 

  • Mardi 2 Septembre

    • à 10h, Amphithéatre Herbrand (1er étage)


      Henri LOMBARDI     Laboratoire de Mathématiques de Besançon UMR CNRS 6623

      Une méthode systématique pour interpréter avec une sémantique constructive les outils de l'algèbre abstraite.

      Résumé : L'algèbre abstraite contemporaine utilise systématiquement des outils non constructifs comme l'axiome du choix et le principe du tiers exclu. Cependant lorsqu'à la fin de la fable est demontrée l'existence d'un objet concret, on finit en général par découvrir un algorithme pour construire cet objet. Nous proposons de déchiffrer ce mystère. Pour cela nous relisons les preuves abstraites au sujet des objets idéaux comme des preuves concrètes au sujet de spécifications incomplètes (qui sont des objets finis concrets) de ces objets idéaux.
       
       

    • à 15 h, Salle de Séminaires (3ème étage)


      Martin HOFMANN     Université de Munich

      Static prediction of heap-space usage of first-order functional programs
      (joint work with Steffen Jost)     

      Résumé : We show how to efficiently obtain linear a priori bounds on the heap space consumption of first-order functional programs using linear programming. The analysis takes memory management either by garbage collection or by explicit deallocation into account. It covers a wide variety of examples including, for instance, the familiar sorting algorithms for lists.

      Our analysis is not restricted to linearly typed functional programs but requires a semantic condition for nonlinear ones which states that only the last of multiple uses of the same variable may be modifying. This semantic condition is formulated with respect to a standard operational semantics and can be guaranteed by a number of existing analyses and type systems, in particular but not exclusively linear typing.

      We also show that integral solutions to the linear programs derived correspond to programs that can be evaluated without any operating system support for memory management in the style of Hofmann's LFPL.

      The particular integer linear programs arising in this way are shown to be feasibly solvable under mild assumptions.
       
       


     
     

    Retour à la page d'accueil du Séminaire