Reasoning about hierarchical storage

Amal Ahmed, Limin Jia, David Walker

Research output: Contribution to journalConference article

16 Scopus citations

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 ever, 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.

Original languageEnglish (US)
Pages (from-to)33-44
Number of pages12
JournalProceedings - Symposium on Logic in Computer Science
StatePublished - Sep 1 2003
Event18th Annual IEEE Symposium on Logic in Computer Science - Ottawa, Ont., Canada
Duration: Jun 22 2003Jun 25 2003

All Science Journal Classification (ASJC) codes

  • Software
  • Mathematics(all)

Fingerprint Dive into the research topics of 'Reasoning about hierarchical storage'. Together they form a unique fingerprint.

  • Cite this