A fully abstract trace semantics for general references

Research output: Chapter or section in a book/report/conference proceedingChapter or section

41 Citations (SciVal)


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.

Original languageEnglish
Title of host publicationAutomata, Languages and Programming
Subtitle of host publicationProceedings of 34th International Colloquium, ICALP 2007, Wrocław, Poland, July 9-13, 2007
EditorsL. Arge, C. Cachin, T. Jurdziński, A. Tarlecki
Place of PublicationBerlin, Germany
PublisherSpringer Verlag
Number of pages13
ISBN (Print)9783540734192
Publication statusPublished - Jul 2007
Event34th International Colloquium on Automata, Languages and Programming, ICALP 2007 - Wroclaw, Poland
Duration: 9 Jul 200713 Jul 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)


Conference34th International Colloquium on Automata, Languages and Programming, ICALP 2007


Dive into the research topics of 'A fully abstract trace semantics for general references'. Together they form a unique fingerprint.

Cite this