Bidomains and full abstraction for countable nondeterminism

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)

Abstract

We describe a denotational semantics for a sequential functional language with random number generation over a countably infinite set (the natural numbers), and prove that it is fully abstract with respect to may-and-must testing. Our model is based on biordered sets similar to Berry's bidomains, and stable, monotone functions. However, (as in prior models of unbounded non-determinism) these functions may not be continuous. Working in a biordered setting allows us to exploit the different properties of both extensional and stable orders to construct a Cartesian closed category of sequential, discontinuous functions, with least and greatest fixpoints having strong enough properties to prove computational adequacy. We establish full abstraction of the semantics by showing that it contains a simple, first-order "universal type-object" within which all types may be embedded using functions defined by (countable) ordinal induction.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures
Subtitle of host publicationProceedings of the 9th International Conference, FOSSACS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software , ETAPS 2006 Vienna, Austria, March 2006
EditorsL. Aceto, A. Ingolfsdottir
Place of PublicationBerlin, Germany
PublisherSpringer Verlag
Pages352-366
Number of pages15
ISBN (Print)9783540330455
DOIs
Publication statusPublished - 2006
Event9th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2006. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006 - Vienna, Austria
Duration: 25 Mar 200631 Mar 2006

Publication series

NameLecture Notes in Computer Science
Volume3921

Conference

Conference9th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2006. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006
CountryAustria
CityVienna
Period25/03/0631/03/06

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Fingerprint Dive into the research topics of 'Bidomains and full abstraction for countable nondeterminism'. Together they form a unique fingerprint.

  • Cite this

    Laird, J. (2006). Bidomains and full abstraction for countable nondeterminism. In L. Aceto, & A. Ingolfsdottir (Eds.), Foundations of Software Science and Computation Structures: Proceedings of the 9th International Conference, FOSSACS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software , ETAPS 2006 Vienna, Austria, March 2006 (pp. 352-366). (Lecture Notes in Computer Science ; Vol. 3921 ). Springer Verlag. https://doi.org/10.1007/11690634_24