TY - CHAP
T1 - A calculus of coroutines
AU - Laird, J.
PY - 2004
Y1 - 2004
N2 - We describe a simple but expressive calculus of sequential processes, which are represented as coroutines. This calculus can be used to express a variety of programming language features; we give simple macros for 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 evaluation trees, which are infinitary normal forms for the calculus. We show that our categorical model can be used to interpret the untyped λ-calculus and use this fact to extract a sound translation of the λ-calculus into our calculus of coroutines.
AB - We describe a simple but expressive calculus of sequential processes, which are represented as coroutines. This calculus can be used to express a variety of programming language features; we give simple macros for 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 evaluation trees, which are infinitary normal forms for the calculus. We show that our categorical model can be used to interpret the untyped λ-calculus and use this fact to extract a sound translation of the λ-calculus into our calculus of coroutines.
UR - http://www.scopus.com/inward/record.url?scp=35048872796&partnerID=8YFLogxK
UR - http://dx.doi.org/10.1007/978-3-540-27836-8_74
U2 - 10.1007/978-3-540-27836-8_74
DO - 10.1007/978-3-540-27836-8_74
M3 - Chapter or section
AN - SCOPUS:35048872796
SN - 9783540228493
T3 - Lecture Notes in Computer Science
SP - 882
EP - 893
BT - Automata, Languages and Programming
A2 - Diaz, J.
A2 - Karhumaki, J.
A2 - Lepisto, A.
A2 - Sannella, D.
PB - Springer Verlag
CY - Berlin, Germany
ER -