Résumés
-------


o Laurent Régnier, "Constructions d'algèbres de Hopf"

Résumé: ça va être chouette


o Jean-Yves Moyen, "Graphes de contrôle de ressources"

Résumé: ça va être très chouette


o Yves Lafont, "Théorie algébrique des circuits booléens" 

Résumé: On va s'amuser avec de jolis diagrammes représentant des
matrices à coefficients dans le corps à 2 éléments. Il y aura plein de
générateurs et de relations. On va même descendre des escaliers pour
arriver à la forme normale. Vous allez voir : ça va être vraiment
chouette !


o Marc de Falco, "Partages en lambda-calcul et geometrie de
	  l'interaction : de bonnes erreurs"  

Résumé: A travers l'exemple du calcul de n^n dans les entiers de
Church, on illustrera explicitement un cas où la géometrie de
l'interaction ne "marche pas", au sens où elle ne coincide pas avec la
beta reduction. On etudiera dans un premier temps où se situe
"l'erreur" pour de petits n, puis on verra comment calculer d'un coup
la semantique de gdi d'une famille de termes arbitrairement grands.


o Damiano Mazza, "Observational Equivalence and the Full Abstraction
          Problem for the Interaction Combinators"  

Résumé: We define a notion of observational equivalence for the
interaction combinators, similar to head-normalization equivalence in
the lambda-calculus, and study the problem of finding a fully-abstract
denotational semantics for it.  The task is rendered particularly
delicate by the presence of phenomena like the "infinite
eta-expansion" present in the lambda-calculus.  This brings us to
introducing "edifices", which are the interaction combinators'
equivalent of Boehm trees.  A fundamental feature of edifices is that
they are metric spaces; it is precisely by exploiting the metric
structure of edifices that one obtains a full-abstraction result: two
nets of interaction combinators are observationally equivalent iff
they have the same edifice.



o Aurélien Pardon, "Une explication du critere de Danos-Regnier pour MLL" 

Résumé: Les représentations graphiques des preuves de la logique
linéaire, les proof-nets, permettent de s'abstraire de contraintes
inhérentes au calcul des séquents comme la syntaxe et les règles
structurelles. La correction (ou prouvabilité) de tels réseaux peut se
vérifier à l'aide de critères purement graphiques, comme le critère de
Danos-Regnier. Sa simplicité en fait le rend très efficace mais peu
compréhensible. Pour donner une preuve de complétude d'un tel critère
et tenter de l'expliquer, nous utiliserons une logique différente :
MILL. Dans ce système intuitionniste, les règles logiques sont des
règles de typage d'un lambda-calcul et les réseaux de preuves ses
arbres de syntaxe. Le critère de Danos-Regnier nous permettra de
construire un lambda-terme typable à partir du réseau de preuve,
assurant ainsi sa validité.




o Paul-André Melliès, "Functorial boxes in string diagrams"

String diagrams were introduced by Roger Penrose as
a handy notation to manipulate morphisms in a monoidal category.
In principle, this graphical notation should encompass the various
pictorial systems introduced in proof-theory
(like Jean-Yves Girard's proof-nets) and
in concurrency theory (like Robin Milner's bigraphs).
This is not the case however, at least because string diagrams
do not accomodate boxes --- a key ingredient in these pictorial systems.

In this short tutorial, based on our accidental rediscovery
of an idea by Robin Cockett and Robert Seely,
we explain how string diagrams may be extended with a notion
of functorial box to depict a functor separating an inside world
(its source category) from an outside world (its target category).

We expose two elementary applications of the notation:
first, we characterize graphically when a faithful balanced
monoidal functor~ F:C -> D transports a trace operator
from the category D to the category C, and we then exploit this
to construct well-behaved fixpoint operators
in cartesian closed categories generated by models of linear logic;
second, we explain how the categorical semantics of linear logic
induces that the exponential box of proof-nets decomposes
as two enshrined functorial boxes.


o Samuel Mimram, "Une théorie algébrique de la sémantique des jeux"

Résumé: chouette et instructif à la fois


o Joachim de Lataillade, "Les modèles de jeux du second ordre et les
	     isomorphismes à la Curry"   

Résumé: ça va être incroyablement chouette


o Lionel Vaux, "Polarized differential nets and non-deterministic
	 choice on stacks"  

Résumé: On présente une chouette extension polarisée des réseaux
d'interaction différentiels avec promotion, où la contraction est
généralisée à toutes les formules négatives (comme dans LLP) et la
co-contraction (celle des réseaux différentiels) est généralisées à
toutes les formules positives.

Le lambda-mu-calcul différentiel ne fait pas usage de cette dernière:
il correspond plutôt aux réseaux obtenus en ajoutant les cellules et
réductions des réseaux différentiels aux réseaux polarisés. En ce
sens, il n'introduit pas grand chose de neuf du point de vue des
réseaux.

On essaie donc de comprendre quel sens calculatoire on peut donner à
la co-contraction sur les types positifs en définissant une extension
du lambda-bar-mu-calcul avec une opération de produit sur les
piles. Ce produit correspond à un choix non déterministe de
l'environnement d'exécution et se comporte comme un produit de
convolution.



o Olivier Laurent, "Concurrence et séquentialité dans les réseaux
	  d'interaction différentiels" 

Résumé: On montre comment les réseaux d'interaction différentiels
permettent de coder suffisamment de primitives de calcul concurrentes
et séquentielles pour encoder des algèbres de processus finitaires
(sans réplication ni définition récursive). On traitera notamment le
cas de CCS, du pi-calcul, du calcul des solos, ...



o Luigi Santocanale, "Topological Properties of Event Structures" 

Résumé: il n'y a vraiment pas plus chouette


o Samuel Hym, "Contrôle de la mobilité par typage dans un calcul réparti"

Résumé: grave chouette


o Silvano dal Zilio, "A Concurrent Calculus with Atomic Transactions"  

Résumé: chouette à souhait