Séminaire des équipes de recherche
An equational presentation of the local state monad
- Date : 21/09/2015
- Lieu : Paris-Rocquencourt - Amphi Turing du bâtiment 1 - 10h30
- Intervenant(s) : Kenji Maillard
In order to account for effects in lambda calculus, monads were introduced by Moggi along with the computational lambda-calculus. Plotkin then introduced algebraic effects as a special class of monads having a presentation as an equational theory in order to reflect more syntactically the operations from programming languages.
In the same strand of research, he also introduced with Power a monad accounting for memory accesses as well as dynamic allocation called the local state monad. A presentation of this monad in term of operations was given later by Staton in the setting of nominal-enriched theories and Melliès in the setting of theories with arity.
In the course of my master studies, I have been working under the supervision of Paul-André Melliès on the local state monad. I will present how this monad can be presented by operations and how it can be seen as some kind of monad transformer over the global state monad, dynamically allocating and deallocating effects as needed.