Certifying Compilation for a Language with Stack Allocation
- 11 October 2006
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10436871,p. 407-416
- https://doi.org/10.1109/lics.2005.9
Abstract
This paper describes an assembly-language type system capable of ensuring memory safety in the presence of both heap and stack allocation. The type system uses linear logic and a set of domain-specific predicates to specify invariants about the shape of the store. Part of the model for our logic is a tree of "stack tags" that tracks the evolution of the stack over time. To demonstrate the expressiveness of the type system, we define Micro-CLI, a simple imperative language that captures the essence of stack allocation in the common language infrastructure. We show how to compile well-typed Micro-CLI into well-typed assembly.Keywords
This publication has 15 references indexed in Scilit:
- L3: A Linear Language with LocationsPublished by Springer Nature ,2005
- Reasoning about hierarchical storagePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Separation logic: a logic for shared mutable data structuresPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- The logical approach to stack typingPublished by Association for Computing Machinery (ACM) ,2003
- Region-based memory management in cyclonePublished by Association for Computing Machinery (ACM) ,2002
- Stack-based typed assembly languageJournal of Functional Programming, 2002
- BI as an assertion language for mutable data structuresPublished by Association for Computing Machinery (ACM) ,2001
- The Logic of Bunched ImplicationsBulletin of Symbolic Logic, 1999
- From system F to typed assembly languageACM Transactions on Programming Languages and Systems, 1999
- Better static memory managementPublished by Association for Computing Machinery (ACM) ,1995