Modules over Monads and Operational Semantics
André Hirschowitz, Tom Hirschowitz, Ambroise Lafont · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2020
This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about (abstract) programming languages or calculi. Generalising the reduction monads of Ahrens et al., we introduce transition monads, thus covering new applications such as ̅λμ-calculus, π-calculus, Positive GSOS specifications, differential λ-calculus, and the big-step, simply-typed, call-by-value λ-calculus. Finally, we design a suitable notion of signature for transition monads.