Paper Info
Title
An Algebraic Account of References in Game Semantics
Abstract
We study the algebraic structure of a programming language with higher-order store, in the style of ML references. Instead of working directly on the operational semantics of the language, we consider its fully abstract game semantics defined by Abramsky, Honda and McCusker one decade ago. This alternative description of the language is nice and conceptual, except on one significant point: the interactive behavior of the higher-order memory cell is reflected in the model by a strategy cell whose definition remains slightly enigmatic. The purpose of our work is precisely to clarify this point, by providing a neat algebraic definition of the strategy. This conceptual reconstruction of the memory cell is based on the idea that a general reference behaves essentially as a linear feedback (or trace operator) in an ambient category of Conway games and strategies. This analysis leads to a purely axiomatic proof of soundness of the model, based on a natural refinement of the replication modality of tensor logic.
Year
DOI
Venue
2009
10.1016/j.entcs.2009.07.099
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
compact-closed categories,higher-order store,replication modality,algebraic structure,operational semantics,memory access,general references,higher-order memory cell,strategy cell,abstract game semantics,programming language,memory access.,trace operator,game semantics,memory cell,neat algebraic definition,tensor logic,conceptual reconstruction,algebraic account,higher order
Operational semantics,Algebraic structure,Computer science,Denotational semantics,Action semantics,Theoretical computer science,Soundness,Game semantics,Well-founded semantics,Algebraic definition
Journal
Volume
ISSN
Citations 
249,
Electronic Notes in Theoretical Computer Science
4
PageRank 
References 
Authors
0.43
19
2
Name
Order
Citations
PageRank
Paul-andré Melliès139230.70
Nicolas Tabareau224123.63