Reasoning about Hierarchical Storage

11 years 5 months ago
Reasoning about Hierarchical Storage
In this paper, we develop a new substructural logic that can encode invariants necessary for reasoning about hierarchical storage. We show how the logic can be used to describe the layout of bits in a memory word, the layout of memory words in a region, the layout of regions in an address space, or even the layout of address spaces in a multiprocessing environment. We provide a semantics for our formulas and then apply the semantics and logic to the task of developing a type system for Mini-KAM, a simplirsion of the abstract machine used in the ML Kit with regions.
Amal J. Ahmed, Limin Jia, David Walker
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where LICS
Authors Amal J. Ahmed, Limin Jia, David Walker
Comments (0)