Resource typing in Guru

12 years 10 months ago
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
Aaron Stump, Evan Austin
Added 17 Mar 2010
Updated 17 Mar 2010
Type Conference
Year 2010
Where PLPV
Authors Aaron Stump, Evan Austin
Comments (0)