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 language | English (US) |
---|---|
Pages (from-to) | 33-44 |
Number of pages | 12 |
Journal | Proceedings - Symposium on Logic in Computer Science |
State | Published - 2003 |
Event | 18th Annual IEEE Symposium on Logic in Computer Science - Ottawa, Ont., Canada Duration: Jun 22 2003 → Jun 25 2003 |
All Science Journal Classification (ASJC) codes
- Software
- General Mathematics