Sound Operational Game Semantics in Type Theory
Peio Borthelle
Inria, ÉNS de Lyon
https://peio.scryk.net/
Date(s) : 18/06/2026 iCal
11h00 - 12h30
Operational Game Semantics (OGS) is a flexible method for building models for open programs based on their operational semantics. After motivating and giving a high-level overview of an OGS model, I will present the most important constructions from my PhD thesis. This will encompass: a high-level axiomatization of abstract machines, used to build a (reasonably) language-generic OGS model; a practical representation 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.
Emplacement
I2M Luminy - TPR2, Salle de Séminaire 304-306 (3ème étage)
Catégories
