Sequentiality and the CPS Semantics of Fresh Names

We investigate the domain-theoretic denotational semantics of a CPS 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 l 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 s” and bistable functions — and prove that it is fully abstract der four (our main result), but that full abstraction fails at order five.

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: James Laird
• Keywords: Abstract Cps Translation, Domain-theoretic Denotational Semantics, ENTCS 2007, first-class Continuations