A theory of indirection via approximation

Aquinas Hobor, Robert Dockins, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

12 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationPOPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages171-184
Number of pages14
DOIs
StatePublished - Apr 20 2010
Event37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10 - Madrid, Spain
Duration: Jan 17 2010Jan 23 2010

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Other

Other37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10
CountrySpain
CityMadrid
Period1/17/101/23/10

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Indirection theory
  • Step-indexed models

Fingerprint Dive into the research topics of 'A theory of indirection via approximation'. Together they form a unique fingerprint.

  • Cite this

    Hobor, A., Dockins, R., & Appel, A. W. (2010). A theory of indirection via approximation. In POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 171-184). (Conference Record of the Annual ACM Symposium on Principles of Programming Languages). https://doi.org/10.1145/1706299.1706322