The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
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).