Sequentiality and the CPS semantics of fresh names

Research output: Contribution to journalArticle

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.

Original languageEnglish
Pages (from-to)203-219
Number of pages17
JournalElectronic Notes in Theoretical Computer Science
Volume173
DOIs
Publication statusPublished - 2 Apr 2007

Keywords

  • Continuation-passing style
  • FM-sets
  • Fresh names
  • Full Abstraction
  • Sequentiality

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Fingerprint Dive into the research topics of 'Sequentiality and the CPS semantics of fresh names'. Together they form a unique fingerprint.

  • Cite this