Séminaire Logique et Interactions
Organisateur: | Lionel Vaux, (tél: +33 4 91 26 96 87) |
---|---|
Lieu: |
I2M, site de Luminy Bâtiment TPR2, CNRS Salle de Séminaires: 3ème étage (304-306). |
Horaire: | en général le jeudi à 11h |
Calendrier partagé au format ICal
Pour vous inscrire à la liste de diffusion, contactez l’organisateur.
29 avril 2021, 10:30 : Séminaire
- Ambroise Lafont (Cogent team, Sydney), (à préciser)
27 mai 2021, 10:30 : Séminaire
- Guilhem Jaber (LS2N, Nantes), Compositional relational reasoning via operational game semantics
-
We use operational game models as a guide to develop relational techniques for establishing contextual equivalences with respect to contexts drawn from a hierarchy of four call-by-value higher-order languages, with either general or ground-type references and with either call/cc or no control operator. In game semantics, the differences between the contexts can be captured by the absence or presence of the O-visibility and O-bracketing conditions.
The proposed technique, which we call Kripke Normal-Form Bisimulations, combines insights from normal-form bisimulation and Kripke-style logical relations with game semantics. In particular, the role of the heap is abstracted away using Kripke-style world transition systems. The differences between the four kinds of contexts manifest themselves through simple local conditions that can be shown to correspond to O-visibility and O-bracketing, where applicable.
The technique is sound and complete by virtue of correspondence with operational game semantics. Moreover, the framework developed in the paper sheds a new light on other related developments, such as backtracking and private transitions in Kripke logical relations, which can be related to specific phenomena in game models.
24 juin 2021, 10:30 : Séminaire
- Pierre Clairambault (LIP, ÉNS Lyon), (à préciser)
8 juillet 2021, 10:30 : Séminaire
- Wesley Fussner (Laboratoire Dieudonné, Université Côte d'Azur), (à préciser)