Modules over monads and operational semantics (expanded version)
Andr\'e Hirschowitz, Tom Hirschowitz, Ambroise Lafont
TL;DR
This paper introduces transition monads as a generalization of reduction monads, providing a high-level mathematical framework to specify and reason about various programming languages and calculi.
Contribution
It generalizes reduction monads to transition monads, enabling applications to a broader range of programming languages and calculi with a unified approach.
Findings
Transition monads cover lambda-calculus, pi-calculus, and more.
A suitable notion of signature for transition monads is designed.
The framework facilitates high-level reasoning about programming languages.
Abstract
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 lambda-bar-mu-calculus, pi-calculus, Positive GSOS specifications, differential lambda-calculus, and the big-step, simply-typed, call-by-value lambda-calculus. Moreover, we design a suitable notion of signature for transition monads.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.