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}