An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on(…)
summary
Paper gives a concrete equational axiomatization for dynamic threads: a parameterized algebraic theory (using presheaves and strong monads) that encodes fork/wait/stop/act and proves completeness by a normal‑form rewriting argument. Terms correspond exactly to pomsets with holes, captured by nine equations, and the denotational model (presheaf/monad-based) is sound and adequate for the operational pool semantics and fully abstract at first order. Practical examples show copied continuations and dropped actions behave as predicted.
AI-written summary · about
chapters (13)
- 0:00Welcome
- 0:22Dynamic thread semantics
- 1:08Pomsets for concurrency
- 4:01Core language with fork
- 8:17Thread IDs semilattice
- 9:00Algebraic effects
- 11:29Equational theory of threads
- 12:57Completeness theorem
- 14:23Terms with free variables
- 17:36Graphical terms
- 19:03Denotational vs operational
- 19:45Summary and future
- 21:11Question and answer session
related talks
44mCAN WE FREE CONCURRENT PROGRAMMING FROM THE MONADIC STYLE
19mScenario-based Proofs for Concurrent Objects
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
21mA Navigation Logic for Recursive Programs with Dynamic Thread Creation
40mEvolving Clojure with Virtual Threads
15mThread-modular Analysis of Release-Acquire Concurrency
20mCoarser Equivalences for Causal Concurrency
54mReasoning about Progress of Concurrent Objects