An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic TheoriesDistinguished Paper
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' andwait'. 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.
Fri 16 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
14:00 - 15:40 | Monads and EffectsPOPL at Dortoirs Chair(s): Henning Urbat Friedrich-Alexander-University Erlangen-Nürnberg | ||
14:00 25mTalk | An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic TheoriesDistinguished Paper POPL Ohad Kammar University of Edinburgh, Jack Liell-Cock University of Oxford, Sam Lindley University of Edinburgh, Cristina Matache University of Edinburgh, Sam Staton University of Oxford DOI | ||
14:25 25mTalk | Handling Higher-Order Effectful Operations with Judgemental Monadic Laws POPL DOI | ||
14:50 25mTalk | Rows and Capabilities as Modal Effects POPL DOI | ||
15:15 25mTalk | The Relative Monadic Metalanguage POPL Jack Liell-Cock University of Oxford, Zev Shirazi University of Oxford, Sam Staton University of Oxford DOI | ||