一句话：论文用PCM间保持结构的部分函数与分离关系，对并发分离逻辑中的所有权转移进行了代数形式化。
并发分离逻辑以并行组合和框架规则下的状态所有权转移为特征，其所有权转移通常由部分交换幺半群（PCM）刻画，但已有研究多从逻辑角度考察，较少关注代数层面。本文通过PCM之间保持结构的部分函数（即态射）以及一种分离关系，对所有权转移进行代数形式化。分离关系是推广不相交性的二元关系，刻画态射保持结构的输入。两种抽象可简化规约书写，提供在线程状态在所有权转移下保持不变的抽象视图，并支持用户从已有PCM构造新的PCM，从而促进验证。
Concurrent separation logic is distinguished by transfer of state ownership upon parallel composition and framing. The algebraic structure that underpins ownership transfer is that of partial commutative monoids (PCMs). Extant research considers ownership transfer primarily from the logical perspective while comparatively less attention is drawn to the algebraic considerations. This paper provides an algebraic formalization of ownership transfer in concurrent separation logic by means of structure-preserving partial functions (i.e., morphisms) between PCMs, and an associated notion of separating relations. Morphisms of structures are a standard concept in algebra and category theory, but haven't seen ubiquitous use in separation logic before. Separating relations. are binary relations that generalize disjointness and characterize the inputs on which morphisms preserve structure. The two abstractions facilitate verification by enabling concise ways of writing specs, by providing abstract views of threads' states that are preserved under ownership transfer, and by enabling user-level construction of new PCMs out of existing ones.
@article{paperbot1197,
title = {On algebraic abstractions for concurrent separation logics},
author = {František Farka and Aleksandar Nanevski and Anindya Banerjee and Germán Andrés Delbianco and Ignacio Fábregas},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434286}
}