Date Added: Jan 2010
This paper presents a resource typing framework for the Guru verified-programming language, in which abstractions for various kinds of program resources can be defined. Implemented examples include reference-counted data, mutable arrays, and heap-allocated mutable aliased data. The approach enables efficient, type-safe programming with mutable and aliased data structures, with explicit deallocation (not garbage collection). The authors evaluate performance of the approach with two verified benchmarks, one involving mutable arrays, and another involving FIFO queues.