一句话：用参数化代数理论给出 fork/wait 动态线程的完备等式公理，并构造一阶全抽象的并发达标语义。
本文研究动态线程并发原语的等式理论。作者基于代数效应与参数化代数理论，将名字与绑定纳入强单子的具体语法，从 fork、wait 及基本原子动作出发建立公理，并以带标号偏序集（pomsets）作为并发模型。该公理化在两种意义下完备：对闭表达式，它精确刻画标号偏序集相等，即模型完备；对开表达式，若在所有闭合替换下相等则可证相等，即语法完备。作者进一步将分析扩展到简单并发语言，给出操作语义与指称语义，并证明该指称语义相对于一阶标号偏序集观察是可靠、充分且全抽象的。
We use the theory of algebraic effects to give a complete equational axiomatization for dynamic threads. Our method is based on parameterized algebraic theories, which give a concrete syntax for strong monads on functor categories, and are a convenient framework for names and binding. Our programs are built from the key primitives ‘fork’ and ‘wait’. ‘Fork’ creates a child thread and passes its name (thread ID) to the parent thread. ‘Wait’ allows us to wait for given child threads to finish. We provide a parameterized algebraic theory built from fork and wait, together with basic atomic actions and laws such as associativity of ‘fork’. Our equational axiomatization is complete in two senses. First, for closed expressions, it completely captures equality of labelled posets (pomsets), an established model of concurrency: model complete. Second, any two open expressions are provably equal if they are equal under all closing substitutions: syntactically complete. The benefit of algebraic effects is that the semantic analysis can focus on the algebraic operations of fork and wait. We then extend the analysis to a simple concurrent programming language by giving operational and denotational semantics. The denotational semantics is built using the methods of parameterized algebraic theories and we show that it is sound, adequate, and fully abstract at first order for labelled-poset observations.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2602-05850,
title = {An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories},
author = {Ohad Kammar and Jack Liell-Cock and Sam Lindley and Cristina Matache and Sam Staton},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776706}
}