Institut de Mathématiques de Luminy
SÉMINAIRES 2004
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 14 décembre
----- à 14 h -----
salle des séminaires

Patrick BAILLOT (
LIPN, Paris 13) :
Des types light pour la réduction en temps polynomial en lambda-calcul.
(travail en collaboration avec Kazushige Terui)

mardi 7 décembre
----- à 14 h -----
salle des séminaires

Dan GHICA (
Oxford University Computing Laboratory) :
Program verification and analysis using game semantics.

Résumé :
In this talk I will introduce the programming language Idealised Concurrent Algol and it's game semantics. The first part of the talk will examine a resource-sensitive type system which identifies a non-trivial finitary fragment of the language, with applications to automated verification. The second part of the talk will describe an augmented game semantics which gives a quantitative model of the language, model shown to be fully abstract relative to Sands's operational notion of improvement.

mardi 16 novembre
Amphithéâtre

Journée "Logiques spatiales".

avec Thomas EHRHARD (IML Marseille), Silvano DAL ZILIO (LIF Marseille), Didier GALMICHE, (LORIA, Nancy), Daniel HIRSCHKOFF (ENS Lyon), Etienne LOZES (ENS Lyon), Laurent REGNIER (IML Marseille), Jean-Marc TALBOT (LIF Lille).

lundi 8 novembre
----- à 14 h -----
Amphithéâtre

Alexis SAURIN
(ENS + INRIA-futur au LIX) :
Séparation en Lambda-mu-calcul.

Résumé :
Après avoir rappelé les bases du lambda-mu-calcul introduit par Michel Parigot pour étendre l'isomorphisme de Curry-Howard à la déduction naturelle classique, je présenterai un résultat de René David et Walter Py montrant que la propriété de séparation (souvent appelée théorème de Böhm) n'est pas vérifiée en lambda-mu-calcul.
On tâchera ensuite de retrouver cette propriété en analysant ce qui, dans le calcul original, est responsable de la non-séparation. Le calcul obtenu, le Lambda-mu-calcul pour lequel la séparation est satisfaite, sera comparé avec avec la version de Parigot ainsi qu'avec une variante de lambda-mu proposée par Philippe de Groote, on verra en particulier comment Lambda-mu peut-être considéré comme un calcul de termes et de streams de termes.
Pour finir, je discuterai de problèmes de typabilité concernant la séparation dans le Lambda-mu-calcul.

mardi 2 novembre
----- à 14 h -----
Amphithéâtre

Albert Burroni
(PPS, Paris VII) :
Algèbres graphiques et catégorique; application à la récursivité et corécursivité.

lundi 18 octobre
----- à 14 h -----
Amphithéâtre

Alain Colmerauer

(IFM CNRS et Univ. de Provence et de la Méditerranée)
:
Complexité des programmes universels.

Résumé :
Cet exposé est consacré à la définition et au calcul de la complexité de différents programmes universels U pour différentes machines. Cette complexité est d'abord vue comme le nombre moyen d'instructions exécutées par U pour simuler l'exécution d'une instruction d'un programme P ayant pour donnée x.
Pour définir une complexité ne dépendant ni de P ni de x on introduit alors la notion de coefficient d'introspection qui exprime le nombre moyen d'instructions exécutées par $U$ pour simuler l'exécution d'une de ses propres instructions. Nous montrons comment obtenir ce coefficient en calculant une matrice carré dont les éléments sont des nombres d'instructions exécutées lors du déroulement de parties sélectionées du U sur des données sélectionnées. Ce coefficient est alors égal à la plus grande valeur propre de cette matrice.
Nous illustrons l'approche par deux exemples de programmes universels particulièrement efficaces~: l'un pour une machine de Turing à trois symboles (symbole blanc non compris) avec un coefficient d'introspection de 3682,98, l'autre pour une machine arthmétique à adressage indirect avec un coefficient d'introspection de 26,27.

lundi 12 juillet
----- à 10 h -----
Amphithéâtre

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...

vendredi 9 juillet
----- à 10 h -----
Amphithéâtre

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.

mardi 29 juin
----- à 14 h -----
Salle des séminaires

Yves Lafont (
IML) :
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
----- à 14 h -----
Salle des séminaires

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 -----
Amphi Herbrand

Harry Mairson (Brandeis University & Invité IML) :
Linearity, type inference, and normalization:
from impotency to idempotency

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.

mardi 25 mai 2004
----- à 14 h 15 -----
Salle des séminaires
Jean-Yves Girard (IML) :
GoI 4

mardi 18 mai 2004
----- à 10 h -----
Amphi Herbrand

Antoine Rauzy (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ésultats pratiques inquiétants que j'ai obtenus récemment en reprenant une étude probabiliste de sûreté sur une centrale nucléaire japonaise.

lundis 10 et 24 mai 2004
----- 2h30 le matin et 2h30 l'après-midi -----
Amphi Herbrand

Jean-Louis Krivine
(PPS Preuves, Programmes et Systèmes, Paris) :
Réalisabilité en analyse classique et dans ZF.
(cours de l'Ecole Doctorale)

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 16 mars 2004
----- à 14 h -----
Salle des séminaires

Emmanuel Beffara
(PPS 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.

mardi 3 février 2004
----- à 14h -----
Salle des séminaires
Yves Guiraud (Université de 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.

 

EL, le 26 novembre 2004