Guilhem Jaber
LS2N, Nantes
http://guilhem.jaber.fr/
Date(s) : 27/05/2021 iCal
10 h 30 min - 11 h 30 min
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.
Slides: http://perso.ens-lyon.fr/pierre.clairambault/cgc/cgc190321.pdf
Lien en visio-conférence :
https://greenlight.lal.cloud.math.cnrs.fr/b/lio-hdc-jef
Catégories