Responsable / Scientific leader : Patrick Cousot
Les abstractions automatique de l'opérateur pre-tilde (pré-image duale) ne permettent en général pas d'obtenir des résultats satisfaisants, à moins d'utiliser des domaines abstraits relationnels « lourds » (comme les polyèdres). Dans cet exposé nous présenterons, dans un cas simple de propriété temporelle, une sémantique fondée sur les traces qui permet de vérifier la propriété et qui autorise des domaines abstraits plus faciles à utiliser. Nous examinerons les abstractions nécessaires pour arriver à des domaines utilisables, ainsi que les possibilités d'étendre cette sémantique à des cas plus généraux de propriétés temporelles.
In this talk I try to explain the techniques for constructing parallelizing compilers in the last 20 years. Due to lack of precision of dependence information the existing compilers are unable to deliver the desired parallel code. Precise data dependence information is possible to obtain using more precise program analysis. I try to do this starting from the semantics of the sequential program (not from the syntax as in the standard parallelizing compilers) and applying abstract interpretation.
L'utilisation des raisonnements par symetries est assez courante en physique, mecanique, chimie...et assez inexistante en informatique. Il existe pourtant bon nombre de problemes (je m'interesserai principalement a des problemes simples de protocoles pour systemes distribues) tres symetriques (certains des processeurs sont interchangeables, les donnees locales sont interchangeables etc.). L'objet de la presentation sera de montrer, 1) les raisonnements par symetries sont puissants (calculs de niveaux atomiques, notion de spin, couleur etc., principe de Pauli, impossibilites en mecanique classique, raisonnements sur les orbitales en chimie ou en spectroscopie) 2) la theorie mathematique derriere tout cela est tres belle (representation de groupes finis/compacts/de Lie). Elle forme un lien entre la combinatoire et la geometrie. 3) cela s'applique aux systemes dynamiques discrets que sont les machines (en semantique) aussi bien qu'aux systemes dynamiques continus de la mecanique (mais la il y aura probablement plus de conjectures que de theoremes).
I will explain Girard's matrix interpretation of Linear Logic and cut-elimination via the execution formula (the Geometry of Interaction). There will be lots of examples, and if time permits, a few hints on how this relates to Game semantics.
We introduce the notion of exact part of a relation and develop some of its properties. One shows how this concept is related to the classical notion of Galois correspondance. In a second part, one indicates various generalizations and in particular how the notion of ``Galois dicorrespondance'' provides among them a promizing field of study.
Je parlerai de quelques articles presentes durant le workshop "New connections..." a Cambridge d'il y a deux semaines. C'est une theorie de la complexite utilisant une notion de calcul sur des anneaux quelconques (et pas seulement Z/2Z - les booleens) et devant permettre a la longue de resoudre le probleme "P=NP?".
Suite de la séance du 9 février 1996.
Juste quelques preuves dissequees de certains protocoles, des nouvelles idees dans le domaine et des problemes ouverts.
Suite de la séance du 12 avril 1996.