一句话：推广 reduction monad 提出 transition monad，为操作语义提供高层代数规范工具，覆盖多种演算与 GSOS 格式。
本文寻找高效、高层的数学工具来规范并推理抽象编程语言与演算。作者推广 Ahrens 等人的 reduction monad，提出 transition monad，并为其设计合适的 signature 概念，以模块化地组织语法与转移规则。该框架覆盖了 reduction monad 难以处理的新应用，包括 lambda-bar-mu-calculus、pi-calculus、Positive GSOS 规范、differential lambda-calculus，以及大步简单类型按值调用的 lambda-calculus。评估以这些代表性演算和规约格式的案例为主，表明 transition monad 能统一表达多种操作语义风格。
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.
@article{paperbot1674,
title = {Modules over monads and operational semantics (expanded version)},
author = {André Hirschowitz and Tom Hirschowitz and Ambroise Lafont},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:3)2022}
}