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 language | English (US) |
---|---|
Pages (from-to) | 171-184 |
Number of pages | 14 |
Journal | ACM SIGPLAN Notices |
Volume | 45 |
Issue number | 1 |
DOIs | |
State | Published - Jan 2010 |
All Science Journal Classification (ASJC) codes
- General Computer Science
Keywords
- Indirection theory
- Step-indexed models