18th Annual IEEE Symposium on Logic in Computer Science (LICS'03)
Reasoning about Hierarchical Storage
Ottawa, Canada
June 22-June 25
ISBN: 0-7695-1884-2
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 simplified version of the abstract machine used in the ML Kit with regions.
Citation:
Amal Ahmed, Limin Jia, David Walker, "Reasoning about Hierarchical Storage," lics, pp.33, 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03), 2003
Usage of this product signifies your acceptance of the
Terms of Use.
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||