File(s) not publicly available
A calculus of coroutines
journal contribution
posted on 2023-06-07, 23:40 authored by James LairdWe 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 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 latter into our calculus of coroutines.
History
Publication status
- Published
Journal
Theoretical Computer ScienceISSN
03043975Publisher
ElsevierExternal DOI
Issue
2-3Volume
350Page range
275-291Pages
0.0Department affiliated with
- Informatics Publications
Full text available
- No
Peer reviewed?
- Yes
Legacy Posted Date
2012-02-06Usage metrics
Categories
No categories selectedKeywords
Licence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC