DYVERSE

DyVerSe aims to develop a theoretical framework for dynamic/game semantics for programming languages, capturing in one versatile setting a spectrum of computational features, representative of the heterogeneity of software (e.g. higher-order functions, concurrency, probabilities or other quantitative aspects). Our ambition is (1) to help unify denotational semantics by providing the missing link between various incompatible models focusing on specific aspects, and (2) to provide a toolbox to reason compositionally about the dynamic behaviour of programs, with an eye towards specification and verification. Operational semantics is a powerful and extensible methodology, perfectly fit for formalization; on the other hand its deployment often follows from ad-hoc choices. It is tied to syntax and struggles with compositionality. Denotational semantics is syntax-independent, and often more principled. It is a great tool to reason about program equivalence or to prove general properties of languages and inform language design, and it comes with compositional reasoning principles on programs. In exchange, it is more mathematically demanding and it is often quite brittle: distinct fragments of the same language may require radically different representations. Denotational models often concern specific programming features, they are are not usually easily extended or combined. DyVerSe seeks to provide the missing link between the syntax-tied operational semantics and a spectrum of incomparable denotational semantics of restricted scope: a syntax-independent and fine-grained description of program executions which could serve both as a unified compositional operational semantics for a wide array of computing features, and as a bridge between specific denotational models. Besides constructing this missing link, DyVerSe aims to put it to work in order to obtain reasoning principles on high-level effectful programs, permit model extraction for automated program verification, or help put under scrutiny the structures used to eliminate race conditions and ensure harmonious use of resources in languages like Rust (among others). To achieve that, DyVerSe builds on recent developments in Game Semantics. Game semantics departs from mainstream denotational semantics by representing the interactive behaviour of programs rather than merely input/output. It is famous for managing to accommodate multiple programming features (various degrees of state, control operators, evaluation order) in one single unified canvas, for sequential deterministic programs; an achievement which has had a strong impact on semantics and beyond, and for which the founders of game semantics were recently awarded the Alonzo Church Award. Though there are games model beyond the sequential deterministic setting, they are incomparable and do not fit in a unified picture anymore. To that defect, recent work on non-deterministic and probabilistic game semantics propose the diagnosis that traditional game semantics lack the required structure to explicitly represent various branching behaviour (such as parallelism, non-determinism, probabilistic choice). To provide this missing branching structure, we propose to build on Concurrent/Asynchronous games. Concurrent games are a branch of game semantics focusing on representing the causal choices behind program actions rather than merely their observations by execution environments. Pioneered by Abramsky and Melliès, they have recently been actively developed building on new definitions due to Winskel, and are finally catching up in expressivity with traditional models. In DyVerSe we will push the development of concurrent games -- their structure, their use for semantics of combinations of effects, their relationship with operational semantics -- to provide the missing link, and put these structures to work towards better tools to reason on or verify programs.