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.

• Type: Conference
• Year: 2003
• Where: LICS
• Authors: Amal J. Ahmed, Limin Jia, David Walker
• Keywords: Address Spaces, Computer Science, Hierarchical Storage, LICS 2003, Memory Words