In this work we address the problem of proving, by static analysis means, that allocating and deallocating regions in the store provides a safe way to achieve memory management. That is, the goal is to provably ensure that a program does not use pointers into a deallocated region. A well-known approach to this problem is the one of Tofte and Talpin. Our first contribution is to provide a simple proof, by means of a subject reduction property, of type safety for their region calculus. Our second, main contribution is that we actually do this for an extension of Tofte-Talpin's calculus, featuring a primitive construct for deallocating regions, similar to C's free, that allows one to circumvent the strict stack-of-regions discipline enforced in Tofte-Talpin's calculus. Our static analysis consists in a novel type and effect system, extending the one of Tofte and Talpin, where we record deallocation effects. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Boudol, G. (2008). Typing safe deallocation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4960 LNCS, pp. 116–130). https://doi.org/10.1007/978-3-540-78739-6_10
Mendeley helps you to discover research relevant for your work.