Towards a causal and compositional operational semantics of programming languages

In this talk, I will present methods and mathematical tools to give operational, yet compositional, causal models of programming languages, using Winskel's event structures. We first illustrate the methodology on a first-order concurrent programming language, in the setting of weak memory models where causal models turn out to be handy to understand cleanly reorderings operated by the hardware.

We then turn to higher-order languages, such as the π-calculus and the λ-calculus. We show how name binding can be elegantly expressed in the semantics by means of game semantics.

Types, seen as protocols, become games, and (open) programs become strategies. From there, we can build a cartesian-closed category that supports interpretation of higher-order concurrent and nondeterministic computations.

We show we can support interpretations sound and adequate for to may, must and fair convergences, using essential events (unobservable events keeping track of nondeterministic choices)