Resource typing in Guru

This paper presents a resource typing framework for the Guru d-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). We evaluate performance of the approach with two verified benchmarks, one involving mutable arrays, and another involving FIFO queues. Categories and Subject Descriptors D.3.2 [Programming Languages]: Applicative (functional) languages; F.3.1 [Logics and Meanings of Programs]: Mechanical verification; F.4.1 [Mathematical Logic]: Mechanical theorem proving General Terms Languages, Verification Keywords Dependently Typed Programming, Resource Types, Aliasing, Language-Based Verification

• Type: Conference
• Year: 2010
• Where: PLPV
• Authors: Aaron Stump, Evan Austin
• Keywords: General Terms Languages, Mutable Aliased Data, Mutable Arrays, PLPV 2010, Programming Languages