@inbook{9249fdc52dd3414e83b2e3f9a89cb117,
title = "A fully abstract trace semantics for general references",
abstract = "We describe a fully abstract trace semantics for a functional language with locally declared general references (a fragment of Standard ML). It is based on a bipartite LTS in which states alternate between program and environment configurations and labels carry only (sets of) basic values, location and pointer names. Interaction between programs and environments is either direct (initiating or terminating subprocedures) or indirect (by the overwriting of shared locations): actions reflect this by carrying updates to the shared part of the store. The trace-sets of programs and contexts may be viewed as deterministic strategies and counter-strategies in the sense of game semantics: we prove soundness of the semantics by showing that the evaluation of a program in an environment tracks the interaction between the corresponding strategies. We establish full abstraction by proving a definability result: every bounded deterministic strategy of a given type is the trace-set of a configuration of that type.",
author = "J. Laird",
year = "2007",
month = jul,
doi = "10.1007/978-3-540-73420-8_58",
language = "English",
isbn = "9783540734192",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "667--679",
editor = "L. Arge and C. Cachin and T. Jurdzi{\'n}ski and A. Tarlecki",
booktitle = "Automata, Languages and Programming",
note = "34th International Colloquium on Automata, Languages and Programming, ICALP 2007 ; Conference date: 09-07-2007 Through 13-07-2007",
}