Institut de Mathématiques de Luminy

SÉMINAIRES 2003
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.

lundi 8 décembre 2003

----- à 14h -----
Salle de séminaires
Jean-Louis Krivine (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 2003

----- à 10h -----
Amphi Herbrand
Jean-Yves Girard (IML) :
Espaces Cohérents Quantiques (suite).

Nota : L'article "LLcup.ps.gz" est disponible à l'adresse http://iml.univ-mrs.fr/~girard/

mardi 7 octobre 2003

----- à 10h -----
Amphi Herbrand
Pierre Hyvernat (IML) :
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. Ils 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

----- à 14h15 -----
Salle de séminaires
Jean-Yves Girard (IML) :
Espaces Cohérents Quantiques.


mardi 16 septembre 2003

----- à 10h -----
Amphi Herbrand
Kazushige Terui
(Foundations of Informatics Research Division, National Inst. 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 2003

----- à 10h -----
Amphi Herbrand
Henri Lombardi (Lab. Math. 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 démontré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.

----- à 15h -----
Salle de séminaires
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.


jeudi 12 juin 2003
Reporté début à une date ultérieure
----- à 14h -----
Salle de séminaires
Jean-Louis Krivine (Paris VII - PPS) :
L'axiome du choix dépendant et l'horloge
(résumé).

mardi 3 juin 2003
Reporté début septembre
-----
à 14h -----
Salle de séminaires
Henri Lombardi (Labo. Mathématiques Besançon) :
Une méthode systématique pour interpréter avec une sémantique
constructive les outils de l'algèbre abstraite
(résumé).


mardi 6 mai 2003

----- à 10h -----
Groupe de travail
Coin Rencontre LDP (2ème étage)
Silvano dal Zilio (LIF, Univ. Provence, Marseille) :
Le calcul Bleu.


vendredi 21 mars 2003

----- à 14h00 -----
Amphi Herbrand
James Laird (Univ. Sussex (Brighton) et IML) :
A game semantics of linear continuation passing.


les 14, 21, 28 janvier 2003

----- de 10h00 à 12h30 -----
Amphi Herbrand
Thomas Streicher (Université de Darmstadt) :
Basic concepts of categorical logic for computer science,
soit 4 cours sur les thèmes de recherche suivants :

- Constructive type theory ansd its semantics,
- Denotational semantics of functional programming languages,
- Synthetic domain theory and its type theoretic axiomatisation,
- Fully abstract models for sequential languages,
- Derivation of environnement machines from continuation semantics,
- Semantic normalisation proofs.

Nota : Ces cours s'adressent notamment aux étudiants du DEA MDFI et aux scientifiques intéressés par la logique.

Résumé :
Concepts from category theory are useful for providing a general notion of model for constructive logics as used in computer science and mathematics. In particular, I will discuss what is a model for first and higher order intuitionistic logic. On the side of examples I will show how every model of computation (a partial combinatory algebra) can be turned into a model of higher order intuitionistic logic (actually of intuitionistic ZF) in which data types and computable functions between them lives as a full subcategory (i.e. all functions are "computable").


14 janvier 2003

----- à 14h00 -----
Salle de séminaires
Masahiro Hamano (JAIST (Japon), Post-doc IML) :
Toward totality of hypercoherences and MALLP

Résumé :
  In this talk we represent a crucial subcategory of Ehrhard's hypercoherences by series of (generalized) states and co-states which satisfy a certain notion of totality. The representation is done in the framework of iterations of Hyland-Tan's double gluing construction and captures duality in a less graph-theoretical manner. Second, we restrict our attention to hereditary/antihereditary hypercoherences, which model Laurent's MALLP  (linear fragment of polarized linear logic) when lifting operators are interpreted by restriction/completion. By applying our softness techniques  for MALL full completeness of GHCoh (Blute, Hamano and Scott in preparation), we show a relationship between polarized proof-structures and dinatural transformations of polarized functors.

 

EL, le 19 novembre 2003.