单子上的模与操作语义（扩展版）

Cellular Monads from Positive GSOS Specifications

We give a leisurely introduction to our abstract framework for operational semantics based on cellular monads on transition categories. Furthermore, we relate it for the first time to an existing format, by showing that all Positive GSOS specifications generate cellular monads whose free algebras are all compositional. As a consequence, we recover the known result that bisimilarity is a congruence in the generated labelled transition system.

Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method (Long Version)

We study Abramsky's applicative bisimilarity abstractly, in the context of call-by-value $λ$-calculi with algebraic effects. We first of all endow a computational $λ$-calculus with a monadic operational semantics. We then show how the theory of relators provides precisely what is needed to generalise applicative bisimilarity to such a calculus, and to single out those monads and relators for which applicative bisimilarity is a congruence, thus a sound methodology for program equivalence. This is done by studying Howe's method in the abstract.

The semantic marriage of monads and effects

Wadler and Thiemann unified type-and-effect systems with monadic semantics via a syntactic correspondence and soundness results with respect to an operational semantics. They conjecture that a general, "coherent" denotational semantics can be given to unify effect systems with a monadic-style semantics. We provide such a semantics based on the novel structure of an indexed monad, which we introduce. We redefine the semantics of Moggi's computational lambda-calculus in terms of (strong) indexed monads which gives a one-to-one correspondence between indices of the denotations and the effect anno…

Bialgebraic Semantics for String Diagrams

Turi and Plotkin's bialgebraic semantics is an abstract approach to specifying the operational semantics of a system, by means of a distributive law between its syntax (encoded as a monad) and its dynamics (an endofunctor). This setup is instrumental in showing that a semantic specification (a coalgebra) satisfies desirable properties: in particular, that it is compositional. In this work, we use the bialgebraic approach to derive well-behaved structural operational semantics of string diagrams, a graphical syntax that is increasingly used in the study of interacting systems across different d…

智能选择与选择单子

Smart Choices and the Selection Monad

从编程语言视角定义两种支持决策抽象的小型语言，基于选择单子给出操作与指称语义，证明两者一致并建立基础类型上的完全抽象与完备性。

处理选择 Monad（完整版）

Handling the Selection Monad (Full Version)

提出一种受 selection monad 启发的新型代数效应处理器，通过引入选择续延使程序员能编写感知损失的优化算法，并为高阶语言 $λC$ 建立了操作与指称语义及多项性质证明。