An Algebraic Theory for Shared-State Concurrency
summary
Presents a concrete monadic denotational model for a higher‑order language with shared‑state interleaving concurrency, proving a representation theorem that the Plotkin–Power/Abadi–Plotkin equational theory of resumptions maps to a monadic denotation built from finite sets of Brookes‑style traces, where every effect is followed by a possible yield. The main theorem establishes directional adequacy as set containment against standard operational semantics, enabling algebraic proofs of redundant access elimination and other compiler rewrites; model is not fully abstract (yield counting) and targets sequential consistency.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:50Virtues of Algebraic Effects
- 3:20Contextual Equivalence
- 4:36Global-State (Sequential) Denotational Semantics
- 6:10Extends to Shared-State (Concurrency)?
- 8:32Theory of Resumptions
- 9:52Lingering Questions
- 11:44Traces - Interrupted Execution
- 12:42Monad Definition
- 20:15Transformations
- 22:05Very Partial Related Work Timeline
- 27:53Adequacy
related talks
24mAn Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on(…)
23mA Denotational Approach to Release/Acquire Concurrency
19mScenario-based Proofs for Concurrent Objects
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
15mSoundness of Predictive Concurrency Analyses
20mCoarser Equivalences for Causal Concurrency
01h 01mThe Future of Concurrency and Parallelism
01h 00mKeynote Talk: Outcome Logic: a foundational framework for concurrent and probabilistic(…)