Dynamic Versatile Semantics – DYVERSE

The approach followed by DyVerSe belongs to the family of «interactive semantics«, which represent programs not as functions, but through their dynamic behaviour with their execution environment. In particular, «game semantics« represents this interaction in a mathematical language inspired by game theory. The execution is a play in a game between two players, exchanging moves corresponding to observable computational events. In the past, game semantics has had tremendous success in providing a unified representation of several computational effects, in particular for sequential programs.

More precisely, the central tool of DyVerSe is «causal game semantics«, which rests on mathematical structures imported from concurrency theory (so-called «true concurrency« models). Rather than representing execution by listing computational events chronologically, causal game semantics records the causal dependency between events. Capturing (combinations of) computational effects then amounts to understanding, fundamentally, which causal patterns are generated by certain combinations of effects.

More precisely, DyVerSe consists of the following five tasks:

A. Understand and develop certain causal structures prior to their application in game semantics.

B. Model more computational effects, or combinations thereof. A central objective, identified as central challenge, is the combination of { concurrency, mutable state, probabilistic choice }, but DyVerSe goes beyond.

C. Provide better links between causal game semantics and operational semantics of programs.

D. Exploit these connections to study and understand modern type systems with ownership mechanisms (as in Rust) limiting the interference between program phrases.

E. Apply these tools to the analysis and verification of programs, or to logic via the «Curry-Howard correspondence«.

Just before the beginning of DyVerSe, de Visme proposed a notion of event structure able to express the combination of non-deterministic and probabilistic choice in a «true concurrency« fashion, a prerequisite to deal with the combination { concurrency, shared state, probabilistic choice } aimed by DyVerSe.

Beyond probabilistic choice, Clairambault and de Visme had previously constructed a games model for a higher-order programming language with quantum primitives. Recently, they proved that this model is in fact fully abstract, i.e. programs are equal in the model if and only if they are undistinguishable in the syntax. They established a formal connection with the earlier quantum relational model of Pagani, Selinger and Valiron, from which it follows that this model was in fact already fully abstract.

Also aiming to establish links between models, Blondeau-Patissier and Clairambault showed that for total finite innocent strategies, the collapse to the relational model is in fact injective, significantly reducing the distance between these two models.

On the operational front, two works are approaching completion:

Castellan and Clairambault established an operational semantics, formulated as a multi-token geometry of interaction machine, for IPA (a language with higher-order, shared memory and parallelism), with an unfolding theorem to the causal games model. The resulting evaluation machine for IPA has been implemented.

Finally, Castellan has developed another approach to implement causal games. The idea is to avoid the usual denotational definition of the interpretation and present it instead as a monadic translation of the source language. This results in a definition of the interpretation which is more direct and easier to compute, and hints at a new monadic approach for concurrency theory.

The work on DyVerSe has just began, and follows its course.

Recent works have highlighted a convergence between causal games, and developments from «quantitative semantics« inspired from linear logic: one the one hand so-called web-based models (relational models, coherence spaces); and on the other hand, techniques relative to the Taylor expansion of lambda-terms. Aiming towards bridges between semantic models, and beyond its original goals, DyVerSe will study and develop this convergence.

Pierre Clairambault, Marc de Visme: Full abstraction for the quantum lambda-calculus. Proc. ACM Program. Lang. 4(POPL): 63:1-63:28 (2020)

Lison Blondeau-Patissier, Pierre Clairambault: Positional Injectivity for Innocent Strategies. Proc. FSCD 2021.

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.