Please use this identifier to cite or link to this item:
|Title:||A theory of indirection via approximation||Authors:||Hobor, A.
|Issue Date:||2010||Citation:||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.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.