Familial monads and structural operational semantics


Tom Hirschowitz, LAMA Chambéry. 24 mai 2018 10:00 limd
Abstract:

Structural operational semantics is a family of syntactic formats for specifying the operational semantics of programming languages, in the form of a labelled transition system. Fiore and his collaborators have proposed an abstract framework for structural operational semantics based on bialgebras, in which they managed to prove that bisimilarity is a congruence. However, their framework does not scale well to languages with variable binding. We give an abstract account of structural operational semantics based on Weber's parametric right adjoint monads, which encompasses variable binding. On the example of pi-calculus, the key idea is that, while Fiore models the syntax through a monad on a certain presheaf category, we use a subtly different presheaf category inspired by our previous work on sheaf models for concurrent languages. The crucial consequence is that the relevant monad is a parametric right adjoint. This yields a very simple proof of congruence of bisimilarity.