For a new seminar of the proofs and algorithms pole of LIX, we are happy to welcome Francesco Gavazzo.

Link to the online conference

Abstract: Motivated by the study of effectful programming languages and computations, I will introduce the theory of monadic rewriting systems. The latter are rewriting systems whose notion of reduction is effectful, effects being modelled as monads. Such systems are to effectful computations and programming languages what traditional rewriting systems are to pure computations and programming languages. Contrary to what happens in the ordinary operational semantics of monadic programming languages, defining mathematically and operationally meaningful notions of monadic rewriting turns out to be simply not possible for several monads, including the distribution, powerset, reader, and global state monad. This raises the question of when monadic rewriting is possible.

I will answer that question by showing that the so-called weakly cartesian monads precisely describe computational effects for which monadic rewriting is well-behaved. If monads are given as equational theories, as it is in the case of algebraic effects, a sufficient condition ensuring monadic rewriting to be well-behaved can be given by looking at the shape of the theory only: such a condition dates back to an old theory by Guatam and requires equations to be linear. Finally, I will apply the abstract theory of monadic rewriting systems to the call-by-value λ-calculus with algebraic effects, this way obtaining the extension of the well-known confluence and standardisation theorems to an effectful setting.

Next seminar will be on Monday 07 June 2021 at 14h00 by Federico Olimpieri.

The list of next seminars can be found at: https://smimram.gitlabpages.inria.fr/proofs-algorithms/seminar/

The calendar of seminars can be found at: <https://smimram.gitlabpages.inria.fr/proofs-algorithms/seminar/calendar.ics >