BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.3.5//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:9109@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20260618T110000
DTEND;TZID=Europe/Paris:20260618T123000
DTSTAMP:20260618T121311Z
URL:https://www.i2m.univ-amu.fr/evenements/sound-operational-game-semantic
 s-in-type-theory/
SUMMARY:Peio Borthelle (Inria\, ÉNS de Lyon): Sound Operational Game Seman
 tics in Type Theory
DESCRIPTION:Peio Borthelle: Operational Game Semantics (OGS) is a flexible 
 method for building models for open programs based on their operational se
 mantics. After motivating and giving a high-level overview of an OGS model
 \, I will present the most important constructions from my PhD thesis. Thi
 s will encompass: a high-level axiomatization of abstract machines\, used 
 to build a (reasonably) language-generic OGS model\; a practical represent
 ation for games and their strategies\, usable in intensional type theories
  such as Rocq\; a high-level proof sketch of the soundness of our generic 
 OGS model w.r.t. contextual equivalence. 
CATEGORIES:Séminaire,Logique et Interactions
LOCATION:I2M Luminy - TPR2\, Salle de Séminaire 304-306 (3ème étage)\, 1
 63 Avenue de Luminy\, Marseille\, 13009\, France
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=163 Avenue de Luminy\, Mars
 eille\, 13009\, France;X-APPLE-RADIUS=100;X-TITLE=I2M Luminy - TPR2\, Sall
 e de Séminaire 304-306 (3ème étage):geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20260329T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR