Reasoning about hierarchical storage
- 22 December 2003
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
In this paper, we develop a new substructural logic thatcan encode invariants necessary for reasoning about hierarchicalstorage. We show how the logic can be used todescribe the layout of bits in a memory word, the layoutof memory words in a region, the layout of regions in anaddress space, or even the layout of address spaces in amultiprocessing environment. We provide a semantics forour formulas and then apply the semantics and logic to thetask of developing a type system for Mini-KAM, a simplifiedversion of the abstract machine used in the ML Kit withregions.Keywords
This publication has 21 references indexed in Scilit:
- A judgmental reconstruction of modal logicMathematical Structures in Computer Science, 2001
- Logical FrameworksPublished by Elsevier ,2001
- Typed memory management via static capabilitiesACM Transactions on Programming Languages and Systems, 2000
- Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear LogicElectronic Notes in Theoretical Computer Science, 1999
- From system F to typed assembly languageACM Transactions on Programming Languages and Systems, 1999
- Stack-based Typed Assembly LanguagePublished by Springer Nature ,1998
- Region-Based Memory ManagementInformation and Computation, 1997
- Reference counting as a computational interpretation of linear logicJournal of Functional Programming, 1996
- The linear abstract machineTheoretical Computer Science, 1988
- Linear logicTheoretical Computer Science, 1987