A model of cooperative threads

Martín Abadi, Gordon D. Plotkin

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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
Title of host publicationProceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009
Number of pages12
Publication statusPublished - 2009

Fingerprint Dive into the research topics of 'A model of cooperative threads'. Together they form a unique fingerprint.

Cite this