Paper: Reasoning about Hierarchical Storage (at LICS 2003)

Authors: Amal J. Ahmed Limin Jia David Walker

Abstract

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.

BibTeX

  @InProceedings{AhmedJiaWalker-ReasoningaboutHiera,
    author = 	 {Amal J. Ahmed and Limin Jia and David Walker},
    title = 	 {Reasoning about Hierarchical Storage},
    booktitle =  {Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2003)},
    year =	 {2003},
    month =	 {June}, 
    pages =      {33--44},
    location =   {Ottawa, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }