Lundi 3 avril 2000, 11heures
175 rue du Chevaleret 75013 Paris,
Salle iC6
- Attention : salle et horaire exceptionnels -
Patrick Baillot
LFCS, Univ. d'Edimbourg
Sémantique cohérente pour la Logique Linéaire Light
Résumé :
La logique linéaire light (LLL) est une variante de la logique
linéaire dûe à Girard qui capture la classe des fonctions calculables
en temps polynomial. Son élimination des coupures offre en effet une
borne polynomiale et toutes les fonctions de cette classe sont
représentables. Sa petite soeur, la logique linéaire élémentaire
(ELL) caractérise, elle, la classe des fonctions élémentairement
récursives.
J'aborderai dans cet exposé la question de la sémantique
dénotationnelle de ces systèmes. L'objectif est ici de mettre en
évidence un modèle satisfaisant les nouveaux principes structurels
mais qui ne soit pas un modèle de la logique linéaire générale. On
vise ainsi à amener sur le terrain de la sémantique ces
caractérisations de la théorie de la démonstration.
L'approche que je propose est une sémantique cohérente stratifiée:
un objet est une suite d'espaces cohérents et les morphismes sont des
cliques stratifiées, c'est-à-dire que leur image à chaque niveau est
une clique de l'espace en question. Ceci est le cadre donnant une
sémantique des preuves de ELL. On ajoute ensuite une structure
supplémentaire sur les objets, une fonction de taille sur la trame
mesurant la différence entre le nombre d'entrées et le nombre de sorties
sur chaque point/calcul.
Cette information quantitative permet d'isoler une catégorie de cliques
localement bornées interpretant les preuves de LLL (mais pas ELL).
Jeudi 30 mars 2000
pas de séance, mais nous vous invitons à assister aux :
Rencontres franco-japonaises
"Logique et Philosophie des Sciences"
Université Keyo - Université Paris 1
(Sorbonne, 30-31 mars 2000)
Résumé :
http://panoramix.univ-paris1.fr/UFR10/ColKeyo2000.html
Jeudi 23 mars 2000, 11heures
175 rue du Chevaleret 75013 Paris,
Salle 0D9
Jim Laird
Univ. of Sussex
A semantics of locally bound exceptions
Résumé :
A game semantics for a functional language with `ML-style' locally
bound exceptions is presented. It is based on Hyland-Ong style games,
but in addition to relaxing the the constraints which impose functional
behaviour (as in models of other computational effects such as
continuations and references) a new feature is required; `control
pointers' which track the flow of control. A full abstraction result is
proved for an extension of the language and model with ML-style
references.
Jeudi 9 mars 2000, 11heures
175 rue du Chevaleret 75013 Paris,
Salle 0D9
Jean-Vincent Loddo
PPS
Alpha-Beta, un algorithme polyvalent pour jouer aux échecs
et pour résoudre un but dans un programme logique
Résumé :
La caractérisation sémantique d'un langage logique (pur ou avec
contraintes) en terme d'un jeu à deux joueurs, permet de recycler un des
algorithmes les plus utilisés dans la théorie des jeux combinatoire,
Alpha-Beta, comme moteur de résolution pour les langages logiques.
Les récents et spectaculaires résultats obtenus par les programmes
d'échecs (défaite du champion du monde Kasparov contre le programme Deep
Blue d'IBM) témoignent d'une sorte d'intelligence artificielle acquise par
ces programmes qui, en revanche, est totalement absente des actuels
moteurs de résolution des langages logiques.
On verra dans cet exposé que la capacité d'Alpha-Beta à simplifier le
calcul ou, en d'autres termes, sa capacité d'élaguer les coups
inintéressants, n'est pas intimement liée à un type de jeu ou à un type de
gain particuliers, mais demande juste la présence d'un ordre entre les
valeurs calculées, qu'il s'agisse de naturels, dans le cas des échecs, ou
de substitutions ou contraintes, dans le cas des langages logiques.
Jeudi 2 mars 2000, 11heures
175 rue du Chevaleret 75013 Paris,
Salle 0D9
P-L. Curien, H. Herbelin
resp. PPS, Université Paris 10
Sur la dualité du calcul
Résumé :
Nous présentons une syntaxe LK_mu_mu tilde pour le calcul des séquents
classique (connecteur implication) qui permet via l'isomorphisme de
Curry-Howard d'exhiber des symétries de calcul telles que
programme/contexte et appel par nom / appel par valeur. Dans notre
syntaxe,,choisir la discipline appel par nom / appel par valeur pour
la réduction se ramène à choisir l'une des deux orientations
symétriques d'une paire critique (qui est une version polarisée de
celle de Berardi et Barbanera). Notre analyse nous conduit à
revisiter la question de savoir ce qu'est une syntaxe naturelle
fonctionnelle pour le calcul par valeur.
On définit une traduction du lambda-mu-calcul dans LK_mu_mu tilde et
une traduction de LK_mu_mu tilde dans le lambda-calcul, et nous
retrouvons des traductions CPS connues en composant ces traductions de
manière appropriée.
Jeudi 2 mars 2000, 14heures
175 rue du Chevaleret 75013 Paris,
Salle 0D9
T. Coquand
Université de Chalmers
Calcul des séquents et topologie
Résumé :
On présente la notion d'``entailment relation'' due a Dana Scott, qui
est une généralisation naturelle de la notion de conséquence, relation
utilisée par exemple dans la présentation des domaines, où l'on se
permet d'avoir plusieurs conclusions possibles. On montre comment
cette notion peut être utilisée pour décrire de manière effective
différents espaces topologiques (spectre d'un anneau, spectre réel,
espaces des valuations,...) Des théorèmes d'extension (comme
Hahn-Banach) se formulent alors comme des théorèmes de conservativité
logique. Une application est une lecture constructive d'une preuve
abstraite d'un théorème de Kronecker: xi, yj etant des indéterminées
(i<=n, j<=m), si on définit zk = Sigma xiyj, i+j=k, alors chaque
élément xiyj est entier sur z0,...,z(n+m).
** Séance exceptionnelle **
Lundi 28 février 2000, 11heures
175 rue du Chevaleret 75013 Paris,
* Salle 1C6 *
Viviana Bono
Univ. de Torino
Object Orientation: A Type Perspective
Résumé :
Following the path of recent researches on the topic, we show how
some object-based language features can be happily modeled within some
functional calculi, proved sound with respect to the
``message-not-understood'' error. Then, we approach the more complicated
problem of modeling class constructs, presenting two proposals and
discussing their respective qualities and drawbacks, together with some
future directions we would like to follow to try to better understand
class-based languages.
Jeudi 24 février 2000, 11heures
175 rue du Chevaleret 75013 Paris,
Salle OD4 :
Alexandre Miquel
INRIA Rocquencourt
Modélisation dans les espaces cohérents d'un Calcul des
Constructions avec types intersection et sous-typage
Résumé :
Nous présentons un modèle basé sur les espaces cohérents pour
interpréter de larges théories des types imprédicatives telles que le
Calcul des Constructions avec univers (ECC). Nous montrons qu'un tel
modèle permet également d'interpréter les types intersection et le
sous-typage, ce que nous illustrons en interprétant une variante de ECC
munie d'un lieur de types intersection. En outre, nous proposons une
méthode générale pour modéliser l'imprédicativité dans ce cadre, en
paramétrant le modèle par un espace cohérent arbitrairement grand destiné
à interpréter les programmes du niveau imprédicatif. Comme application,
nous montrons que des types non dénombrables - tels que le type des
nombres réels ou le type des ensembles de Zermelo-Fränkel - peuvent être
axiomatisés au niveau imprédicatif d'une théorie des types telle que ECC
sans mettre en danger la cohérence du système.
Jeudi 17 février 2000, 11heures
175 rue du Chevaleret 75013 Paris,
Salle OD4 :
Michele Bugliesi
Typed Mobile Objects
Résumé :
We describe a general model for embedding object-oriented features in
calculi of mobile agents. The model results from extending agents with
methods and a primitive for method invocation. We then study an typed
instance of this model, called MA++, that is based on Cardelli and
Gordon's calculus of Mobile Ambients. We describe a type system for
MA++, give a proof of Subject Reduction, discuss the use of
the type system to statically detect run-time type errors and hint at
possible richer type systems for program verification.
This is joint work with Giuseppe Castagna, Silvia Crafa and Francesco
Zappa.
Jeudi 27 janvier 2000, pas de séance, mais, le lendemain :
Vendredi 28 Janvier 2000,
175 rue du Chevaleret 75013 Paris,
Salle 1C12 :
soutenances de thèses
Thierry Joly (à 14 heures)
Codages, séparabilité et représentation
de fonctions en lambda-calcul simplement
typé et dans d'autres systèmes de types.
Lorenzo Tortora de Falco (à 16 heures)
Réseaux, cohérence et expériences obsessionnelles
Jeudi 20 janvier 2000, 11 heures,
175 rue du Chevaleret 75013 Paris,
Salle 0D4 (rez-de-chaussee)
Vincent Danos
PPS
Réalisabilité du lambda-c calcul (selon Krivine)
avec application à la recherche de spécification
Jeudi 13 janvier 2000, 11 heures,
175 rue du Chevaleret 75013 Paris,
Salle 0D4 (rez-de-chaussee)
Christian Urban
IML Marseille
Classical Logic and Computation
Résumé :
I shall present a strongly normalising cut-elimination
procedure for classical logic. This procedure is inspired
by work of Danos et al on LK^tq, but does not require their
colour annotations. Due to the generality of the cut-elimination
procedure without colours, strong normalisation is more difficult
to prove. The technology necessary to prove this property will
be outlined in the talk. I will conclude with remarks on the
computational interpretation of classical proofs. In contrast
to proposals given for LK^tq and Parigot's lambda-mu, this
interpretation is not constrained by confluence.
Jeudi 6 janvier 2000, 11 heures,
175 rue du Chevaleret 75013 Paris,
Salle 0D4 (rez-de-chaussee)
Emmanuel Polonovski
PPS
Substitutions explicites et réseaux de preuves
Résumé :
L'extension de l'élimination des coupures dans les
réseaux de preuves de la logique linéaire par une
règle supplémentaire permet de faciliter la simulation
des lambda-calculs avec substitutions explicites. Nous prouvons la
normalisation forte du lambda-calcul grâce à la
traduction et la simulation dans ces réseaux. De plus, nous
proposons une version de ce calcul avec noms.
Jeudi 16 Déembre 1999, 11 heures,
175 rue du Chevaleret 75013 Paris,
Salle 0D4 (rez-de-chaussee)
Jean-Yves Girard
IML, Marseille
Ludique : locatif contre spirituel
Résumé :
la logique usuelle est spirituelle (car elle
réfère à un objet défini à isomorphisme
près). Pourtant on s'aperçoit que la structure ludique
profonde de la logique est en fait locative,
i.e. réfère à un objet dans un lieu
précis.
Le phénomène locatif le plus typique est la capture de
variables (qui ne sont autres que des adresses), et on sait d'ailleurs
comment l'éviter: en renommant les variables, c'est la
alpha-conversion.
La spiritualité logique est donc le résultat de
délocalisations systématiques, par exemple au lieu d'une
union, on prendra une somme disjointe etc.
Que se passe-t-il donc quand on refuse le jeu de la
délocalisation ? Des tas de choses amusantes:
1- les opérations logiques deviennent strictement
associatives, commutatives. Ainsi l'intersection de types et la
conjonction intuitionniste & ne sont plus que les aspects locatif et
spirituel d'une même opération, l'intersection.
2- la seule opération logique locative déjà
connue, la quantification (au moins au second ordre, le cas du premier
ordre étant plus délicat) se met à
différer de son interprétation locative (Tarskienne);
par exemple on obtient des formes prénexes tout à fait
constructives.
3- les formules logiques se mettent à interférer : ainsi la
conjonction A \otime B de formules vraies peut être fausse, et
la conjonction de formules fausses, vraies.
Jeudi 9 Déembre 1999, 11 heures,
175 rue du Chevaleret 75013 Paris,
Salle 0D4 (rez-de-chaussee)
Pascal MANOURY
PPS, Paris 6
Conception et implantation de systèmes d'aide a la preuve.
Résumé :
on se propose de faire un rapide tour d'horizon de quelques
systèmes d'aide au développement de preuves formelles.
Nous passerons en revue quelques formalismes et choix d'implantations
de divers systèmes pour conclure par la présentation de
ce qui nous semble les bons choix pour un système
dédié à la preuve de programmes ML.
Jeudi 2 Déembre 1999, 11 heures,
175 rue du Chevaleret 75013 Paris,
Salle 0D4 (rez-de-chaussee)
Sylvain HUET
Cryo-networks (http://www.cryo-networks.com)
A User-Flow approach for multi-user applications with DMS
(Distributed Modules System)
Résumé :
We have developped tools that bring to non-programmer people the power
to design multi-user applications over internet. Multi-user
application is not only 3d virtual world, it is more generally
application in which people can interact with or through the same
"object". Because they are addressing non-programmer people, these
tools have to hide programming problems as well as distribution
problems. We will describe the DMS architecture and the Scol
programming language on which both tools and applications are based.
Jeudi 18 Novembre 1999, 11 heures,
Campus Jussieu, couloir 55-56 salle 107 (dite le "sous-marin")
-- Séance double --
Olivier LAURENT
IML, Marseille
Analyse du lambda-mu calcul dans les réseaux polarisés
Résumé :
On définit les réseaux polarisés pour le fragment
multiplicatif-exponentiel, puis la traduction du lambda-mu calcul dans
ces réseaux. On montre que cette traduction est un
homomorphisme sur les réductions. On définit ensuite de
manière interne au lambda-mu calcul la relation
d'équivalence (sigma-équivalence) que cette traduction
réalise.
Laurent RÉGNIER
IML, Marseille
Réseaux polarisés, géométrie de l'interaction et
machine de Krivine pour le lambda-mu calcul.
Résumé :
Une adaptation simple de l'algèbre dynamique reposant sur
l'équation de splitting permet de définir la
géométrie de l'interaction des réseaux polarisés
(multiplicatifs-exponentiels). On peut ensuite montrer, d'une
manière similaire à ce qui se passe dans le
lambda-calcul, comment la GoI permet de retrouver la machine de
Krivine pour le lambda-mu calcul.
Jeudi 28 Octobre 1999, 11 heures,
Campus Jussieu, couloir 55-56 salle 107 (dite le "sous-marin")
Jean GOUBAULT-LARRECQ
G.I.E. DYADE
A propos de S4 et d'ensembles simpliciaux augmentés.
Résumé :
Il se trouve qu'il existe des rapports intimes
entre les preuves en logique modale minimale
S4 et la catégorie des ensembles simpliciaux augmentés
(a.s., pour faire bref).
Plus précisément, je montrerai que les premières,
convenablement décrits par un language de style déduction
naturelle etendant le lambda-calcul simplement type,
se plongent strictement dans la catégorie des ensembles
a.s. Les égalités (par conversion) entre preuves sont
préservées sous forme d'égalités entre fonctions a.s.
(correction), et réciproquement deux preuves qui ont
la même interprétation dans tous les modèles a.s. sont
convertibles. Ceci étend un théorème de Friedman dans
le cas non modal d'un côte et ensembliste (non a.s.)
de l'autre.
La logique dont les formules sont les ensembles
a.s. et les preuves sont les fonctions a.s. étend donc
S4 minimale, et offre en fait toute une panoplie de
nouveaux connecteurs logiques. On compte notamment
toutes les modalites de la "tense logic", y compris
des modalités existentielles engendrant des monades
fortes au sens de Moggi; des connecteurs
ayant un goût de sous-structuralité comme la jointure,
de nouvelles modalités comme la subdivision barycentrique
(venant de considérations géometriques) ou des opérateurs
de modélisation de la dynamique de systemes parallèles,
a la Herlihy.
Jeudi 21 Octobre 1999, 11 heures,
Campus Jussieu, couloir 55-56 salle 107 (dite le "sous-marin")
Pierre-Louis CURIEN
PPS, CNRS-Paris 7
SUR L'ÉTA EXPENSION INFINIE
Résumé :
On revient sur la caractérisation classique de l'inégalité
observationnelle fondée sur les formes normales de tête du
lambda-calcul, par un ordre particulier sur les arbres de Boehm qui
met en jeu des éta-expansions infinies. On apporte deux "briquettes"
à ce noble édifice: une interprétation de cet ordre en termes de
jeux, et un résultat de continuité (pour justifier une fraction
finie de l'ordre, on n'a besoin que d'un nombre fini
d'éta-expansions infinies de variables).
Jeudi 14 Octobre 1999, 11 heures,
Campus Jussieu, couloir 55-56 salle 107 (dite le "sous-marin")
Vincent DANOS
PPS-Paris 7
SÉMANTIQUE DE JEUX POUR PCF PROBABILISTE