1 Search Results for "Laird, James D."

Document

DOI: 10.4230/LIPIcs.CSL.2018.24

A Fully Abstract Game Semantics for Countable Nondeterminism

Authors: W. John Gowers and James D. Laird

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract

The concept of fairness for a concurrent program means that the program must be able to exhibit an unbounded amount of nondeterminism without diverging. Game semantics models of nondeterminism show that this is hard to implement; for example, Harmer and McCusker's model only admits infinite nondeterminism if there is also the possibility of divergence. We solve a long standing problem by giving a fully abstract game semantics for a simple stateful language with a countably infinite nondeterminism primitive. We see that doing so requires us to keep track of infinitary information about strategies, as well as their finite behaviours. The unbounded nondeterminism gives rise to further problems, which can be formalized as a lack of continuity in the language. In order to prove adequacy for our model (which usually requires continuity), we develop a new technique in which we simulate the nondeterminism using a deterministic stateful construction, and then use combinatorial techniques to transfer the result to the nondeterministic language. Lastly, we prove full abstraction for the model; because of the lack of continuity, we cannot deduce this from definability of compact elements in the usual way, and we have to use a stronger universality result instead. We discuss how our techniques yield proofs of adequacy for models of nondeterministic PCF, such as those given by Tsukada and Ong.

Cite as

W. John Gowers and James D. Laird. A Fully Abstract Game Semantics for Countable Nondeterminism. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{gowers_et_al:LIPIcs.CSL.2018.24,
  author =	{Gowers, W. John and Laird, James D.},
  title =	{{A Fully Abstract Game Semantics for Countable Nondeterminism}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{24:1--24:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.24},
  URN =		{urn:nbn:de:0030-drops-96918},
  doi =		{10.4230/LIPIcs.CSL.2018.24},
  annote =	{Keywords: semantics, nondeterminism, games and logic}
}

Refine by Author
1 Gowers, W. John
1 Laird, James D.

Refine by Classification

Refine by Keyword
1 games and logic
1 nondeterminism
1 semantics

Refine by Type
1 document

Refine by Publication Year
1 2018

1 Search Results for "Laird, James D."

A Fully Abstract Game Semantics for Countable Nondeterminism

Abstract

Cite as

Thanks for your feedback!

Could not send message