Abstract
We investigate the domain-theoretic denotational semantics of a CPS calculus with fresh name declaration. This is the target of a fully abstract CPS translation from the nu-calculus with first-class continuations. We describe a notion of ``FM-categorical'' model for our calculus, with a simple interpretation of name generation due to Shinwell and Pitts. We show that full abstraction fails (at order two) in the simplest instance of such a model (FM-cpos) because of the presence of parallel elements. Accordingly, we define a sequential model --- FM-biorders, based on ``bistable FM-bicpos'' and bistable functions --- and prove that it is fully abstract up to order four (our main result), but that full abstraction fails at order five.
- Full text (.pdf)
- Bibtex entry:
@Inproceedings{mfps07,
title = "Sequentiality and the CPS semantics of fresh names",
booktitle = "Proceedings of MFPS '07",
series = "ENTCS",
publisher = "Elsevier",
number = 173,
pages = "203 --219",
year = 2007}