Aurore Alcolei (ENS de Lyon), Resource-tracking concurrent games

Schedule

Abstract

In the study of programming languages, denotational semantics is used to abstract away from (some) intermediate steps of computation by providing invariants of reduction. Although these abstractions are very useful to help reasoning about qualitative program behaviours such as program termination, they usually do not reflect quantitative informations such as permissions or time consumption.

In this talk, I will present a framework of annotated concurrent games and strategies on event structures that generally allows for keeping track of side-information, that is, data whose value may vary with the execution flow but cannot modify it. In particular, I will use this new framework to give a sound denotational semantics to R-IPA, an affine concurrent higher-order programming language with shared state and a primitive for resource consumption, parametrized by an algebraic structure R expressing resources. Although this model is not adequate in general – its analysis being finer than that offered by the general operational semantics on resource R – I will show that adequacy holds for an operational semantics specialized to time consumption.