Paper: Certifying Compilation for a Language with Stack Allocation (at LICS 2005)
Authors: Limin Jia Frances Spalding David Walker Neal Glew
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.
BibTeX
@InProceedings{JiaSpaldingWalkerGl-CertifyingCompilati, author = {Limin Jia and Frances Spalding and David Walker and Neal Glew}, title = {Certifying Compilation for a Language with Stack Allocation}, booktitle = {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)}, year = {2005}, month = {June}, pages = {407--416}, location = {Chicago, USA}, publisher = {IEEE Computer Society Press} }