A Model of Cooperative Threads

Martin Abadi, Gordon D. Plotkin

Research output: Contribution to journalArticlepeer-review


We develop a model of concurrent imperative programming with threads. We focus on a small imperative language with cooperative threads which execute without interruption until they terminate or explicitly yield control. We define and study a trace-based denotational semantics for this language; this semantics is fully abstract but mathematically elementary. We also give an equational theory for the computational effects that underlie the language, including thread spawning. We then analyze threads in terms of the free algebra monad for this theory.

Original languageEnglish
Article number2
Pages (from-to)1-39
Number of pages39
JournalLogical Methods in Computer Science
Issue number4
Publication statusPublished - Oct 2010

Cite this