Please use this identifier to cite or link to this item: https://doi.org/10.1145/1706299.1706322
Title: A theory of indirection via approximation
Authors: Hobor, A. 
Dockins, R.
Appel, A.W.
Keywords: Indirection theory
Step-indexed models
Issue Date: 2010
Source: Hobor, A., Dockins, R., Appel, A.W. (2010). A theory of indirection via approximation. Conference Record of the Annual ACM Symposium on Principles of Programming Languages : 171-184. ScholarBank@NUS Repository. https://doi.org/10.1145/1706299.1706322
Abstract: Building semantic models that account for various kinds of indirect reference has traditionally been a difficult problem. Indirect reference can appear in many guises, such as heap pointers, higher-order functions, object references, and shared-memory mutexes. We give a general method to construct models containing indirect reference by presenting a "theory of indirection". Our method can be applied in a wide variety of settings and uses only simple, elementary mathematics. In addition to various forms of indirect reference, the resulting models support powerful features such as impredicative quantification and equirecursion; moreover they are compatible with the kind of powerful substructural accounting required to model (higher-order) separation logic. In contrast to previous work, our model is easy to apply to new settings and has a simple axiomatization, which is complete in the sense that all models of it are isomorphic. Our proofs are machine-checked in Coq. Copyright © 2010 ACM.
Source Title: Conference Record of the Annual ACM Symposium on Principles of Programming Languages
URI: http://scholarbank.nus.edu.sg/handle/10635/40831
ISBN: 9781605584799
ISSN: 07308566
DOI: 10.1145/1706299.1706322
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

9
checked on Dec 14, 2017

WEB OF SCIENCETM
Citations

8
checked on Nov 20, 2017

Page view(s)

47
checked on Dec 10, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.