Séminaire, 10 novembre 2011
Lieu
La rencontre aura lieu à l'École Normale Supérieure de Lyon, campus Jacques Monod, dans l'amphi B le matin et dans l'amphi Schroedinger l'après-midi. Pour venir, voir les instructions sur le site du LIP ou sur un plan, par exemple chez Google Maps. À l'entrée, se présenter à la réception, qui aura la liste des inscrits.
Programme
- 10:30 – 12:00
-
Daniele Varacca (PPS - Université Paris Diderot)
We had given in 2007 a stable event structures semantics of the internal π-calculus. To extend this to the full π-calculus, we needed to deal with
the communication of free names,
the extrusion of bound names.
Free names pose no particular problems, but scope extrusion is tricky, especially if we want to allow parallel extrusions. After years of trying we came to the conclusion that it is not possible to satisfactorily model parallel extrusion within the framework of stable event structures. We propose a semantics that while using unstable structures, in a sense is very close to the stable case. Adequacy theorems and open questions will be provided in great abundance.
This is joint work with Silvia Crafa and Nobuko Yoshida.
- 14:00 – 15:00
-
Thibaut Balabonski (PPS - Université Paris Diderot)
L'objectif est de faire le lien entre deux avatars de la réduction optimale. L'un concerne la réduction faible du λ-calcul, l'autre la récriture du premier ordre, et tous deux se démarquent de la théorie générale par une même agréable propriété : on peut les implémenter simplement avec des graphes acycliques.
Je commencerai par présenter les principes de la réduction optimale tels qu'introduits par Lévy, en insistant sur leurs liens avec les notions d'événement et de causalité.
On interprétera ensuite dans ce cadre le λ-lifting, un procédé de compilation classique assurant le passage du λ-calcul à la récriture du premier ordre. On verra que cette transformation peut être vue comme un événement “silencieux”, causalement transparent, et respectueux de l'optimalité, et on en profitera pour réaliser quelques transferts de propriétés.
- 15:30 – 16:30
-
Stefan Hetzl (PPS - Univsersité Paris Diderot)
Herbrand's theorem states that an existential formula is provable in classical first-order logic iff a finite disjunction of instances is a propositional tautology. This theorem and appropriate extensions of it can be used for representing proofs with and without cuts in a compact way.
I will speak about this representation and its algorithmic advantages in certain classes of proofs: 1) it allows cut-elimination procedures without syntactic bureaucracy and 2) it makes it possible to algorithmically reverse cut-elimination: by finding sufficiently similar parts of a cut-free proof and identifying them by introduction of a cut the proof is abbreviated.
