Paper: A Fully Abstract Game Semantics for Finite Nondeterminism (at LICS 1999)

Authors: Russell Harmer Guy McCusker

Abstract

A game semantics of finite nondeterminism is proposed. In this model, a strategy may make a choice between different moves in a given situation; moreover, strategies carry extra information about their possible divergent behaviour. A Cartesian closed category is built and a model of a simple, higher-order nondeterministic imperative language is given. This model is shown to be fully abstract, with respect to an equivalence based on both safety and liveness properties, by means of a factorization theorem which states that every nondeterministic strategy is the composite of a deterministic strategy with a nondeterministic oracle.

BibTeX

  @InProceedings{HarmerMcCusker-AFullyAbstractGameS,
    author = 	 {Russell Harmer and Guy McCusker},
    title = 	 {A Fully Abstract Game Semantics for Finite Nondeterminism},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1999)},
    year =	 {1999},
    month =	 {July}, 
    pages =      {422--430},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }