Aurore Alcolei
LIP, ENS Lyon
http://perso.ens-lyon.fr/aurore.alcolei/
Date(s) : 23/05/2019 iCal
11 h 00 min - 12 h 30 min
Game semantics is an interactive denotational semantics: a denotation specifies the behaviour of a term/proof with respect to its environment. As such it is one of the most intensional model available in the Curry-Howard community.
Despite their intensional persprective, game models still omit a number of computational informations by hiding away internal reductions. This power of abstraction is at the core of the methodology of denotational semantics in that it aims to provide invariants under reduction. Yet, in some cases, this abstraction is too strong and prevents to capture some desirable informations.
In this talk, I will present how the model of concurrent game and strategies on event structures can be naturally extended with annotations from any (in)equational theory to keep track of side-information, that is information that may vary with interactions but does not influence their outcomes.
Depending on time and audience’s interest, I will present this construction through two independent results: on the logic side I will show how this model instantiated with terms can be used to give a new interpretation and proof of the Herbrand’s theorem; on the programming side I will introduce a semantics for R-IPA, a concurrent programming language with shared memory and an operational semantics keeping track of resource consumption, based on an instantiation of that same model with annotations being functions over reals.
Catégories