The Library
Deconstructing general references via game semantics
Tools
Murawski, Andrzej S. and Tzevelekos, Nikos (2013) Deconstructing general references via game semantics. In: 16th International Conference on Foundations of Software Science and Computation Structures, Rome, Italy., 16-24 Mar 2013. Published in: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Volume 7794 pp. 241-256. ISBN 978-3-642-37074-8. doi:10.1007/978-3-642-37075-5_16 ISSN 0302-9743.
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
Official URL: http://dx.doi.org/10.1007/978-3-642-37075-5_16
Abstract
We investigate the game semantics of general references through the fully abstract game model of Abramsky, Honda and McCusker (AHM), which demonstrated that the visibility condition in games corresponds to the extra expressivity afforded by higher-order references with respect to integer references. First, we prove a stronger version of the visible factorisation result from AHM, by decomposing any strategy into a visible one and a single strategy corresponding to a reference cell of type unit → unit (AHM accounted only for finite strategies and its result involved unboundedly many cells). We show that the strengthened version of the theorem implies universality of the model and, consequently, we can rely upon it to provide semantic proofs of program transformation results. In particular, one can prove that any program with general references is equivalent to a purely functional program augmented with a single unit → unit reference cell and a single integer cell. We also propose a syntactic method of achieving such a transformation. Finally, we provide a type-theoretic characterisation of terms in which the use of general references can be simulated with an integer reference cell or through purely functional computation, without any changes to the underlying types.
Item Type: | Conference Item (Paper) | ||||
---|---|---|---|---|---|
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||
Journal or Publication Title: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | ||||
Publisher: | Springer Berlin Heidelberg | ||||
ISBN: | 978-3-642-37074-8 | ||||
ISSN: | 0302-9743 | ||||
Book Title: | Foundations of Software Science and Computation Structures | ||||
Official Date: | 2013 | ||||
Dates: |
|
||||
Volume: | Volume 7794 | ||||
Page Range: | pp. 241-256 | ||||
DOI: | 10.1007/978-3-642-37075-5_16 | ||||
Status: | Peer Reviewed | ||||
Publication Status: | Published | ||||
Access rights to Published version: | Restricted or Subscription Access | ||||
Conference Paper Type: | Paper | ||||
Title of Event: | 16th International Conference on Foundations of Software Science and Computation Structures | ||||
Type of Event: | Conference | ||||
Location of Event: | Rome, Italy. | ||||
Date(s) of Event: | 16-24 Mar 2013 |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |