We propose a type system for a programming language with memory allocation/deallocation primitives, which prevents memory- related errors such as double-frees and memory leaks. The main idea is to augment pointer types with fractional ownerships, which express both capabilities and obligations to access or deallocate memory cells. By assigning an ownership to each pointer type constructor (rather than to a variable), our type system can properly reason about list/tree-manipulating programs. Furthermore, thanks to the use of fractions as ownerships, the type system admits a polynomial-time type inference algorithm, which serves as an algorithm for automatic verification of lack of memory-related errors. A prototype verifier has been implemented and tested for C programs. © 2009 Springer-Verlag.
CITATION STYLE
Suenaga, K., & Kobayashi, N. (2009). Fractional ownerships for safe memory deallocation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5904 LNCS, pp. 128–143). https://doi.org/10.1007/978-3-642-10672-9_11
Mendeley helps you to discover research relevant for your work.