Abstract
We describe a simple but expressive calculus of sequential processes, represented as coroutines. We show that this calculus can be used to express a variety of programming language features including procedure calls, labelled jumps, integer references and stacks. We describe the operational properties of the calculus using reduction rules and equational axioms.
We describe a notion of categorical model for our calculus, and give a simple example of such a model based on a category of games and strategies. We prove full abstraction results showing that equivalence in the categorical model corresponds to observational equivalence in the calculus, and also to equivalence of \emph{evaluation trees}, which are infinitary normal forms for the calculus.
We show that our categorical model can be used to interpret the untyped lambda-calculus and use this fact to extract a sound translation of the latter into our calculus of coroutines.
- Full text (.pdf) Extended abstract (.pdf) (from ICALP '04).
- Slides (.pdf) from the conference presentation.
- Bibtex entry
> @article{CClong,
author = "J. Laird",
title = "A Calculus of Coroutines",
journal = "Theoretical Computer Science (ICALP '04 special issue)",
volume = 350,
pages = "275--291",
year = 2006}