一句话：将中心性/中心子单子概念推广到对称幺半范畴上的强单子，并建立带中心子单子的λ演算语义的可靠性、完备性与内部语言结果。
单子（monad）是范畴论中建模计算效应的代数结构。本文在对称幺半范畴上为强单子定义“中心”（centre）及更一般的“中心性”，即效应与所有其他效应可交换的性质。作者给出刻画强单子中心存在的三个等价条件，并将其与 Power 和 Robinson 的前幺半中心联系起来；还证明许多常见范畴上的强单子都具有中心，说明该概念具有普遍性。进一步，论文研究中心子单子（必然可交换），为带中心子单子的 λ 演算建立等式理论，给出范畴模型，并证明该语义的可靠性、完备性与内部语言定理。
Monads in category theory are algebraic structures that can be used to model computational effects in programming languages. We show how the notion of "centre", and more generally "centrality", i.e., the property for an effect to commute with all other effects, may be formulated for strong monads acting on symmetric monoidal categories. We identify three equivalent conditions which characterise the existence of the centre of a strong monad (some of which relate it to the premonoidal centre of Power and Robinson) and we show that every strong monad on many well-known naturally occurring categories does admit a centre, thereby showing that this new notion is ubiquitous. More generally, we study central submonads, which are necessarily commutative, just like the centre of a strong monad. We provide a computational interpretation by formulating equational theories of lambda calculi equipped with central submonads, we describe categorical models for these theories and prove soundness, completeness and internal language results for our semantics.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{CaretteLZ23,
title = {Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages},
author = {Titouan Carette and Louis Lemonnier and Vladimir Zamdzhiev},
booktitle = {LICS},
year = {2023},
doi = {10.1109/lics56636.2023.10175687}
}