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.

翻译：我们运用代数效应理论为动态线程提供了一套完整的等式公理化方法。该方法基于参数化代数理论，该理论为函子范畴上的强单子提供了具体语法，并为名称与绑定提供了便捷的框架。我们的程序由核心原语`fork`与`wait`构建而成。`Fork`创建子线程并将其名称（线程ID）传递给父线程。`Wait`允许我们等待指定的子线程完成执行。我们构建了一个由fork和wait组成的参数化代数理论，并包含基本的原子操作及定律（如`fork`的结合律）。我们的等式公理化在两种意义上具有完备性。首先，对于闭表达式，它完全刻画了标记偏序集（pomsets）这一成熟并发模型中的相等关系：模型完备。其次，任何两个开表达式，若在所有闭化替换下均相等，则它们可证相等：语法完备。代数效应的优势在于，语义分析可聚焦于fork与wait的代数运算。随后，我们通过给出操作语义与指称语义，将分析扩展至一个简单的并发编程语言。指称语义采用参数化代数理论的方法构建，并证明其对于一阶标记偏序集观测具有可靠性、充分性及完全抽象性。