Conference proceeding
Resource typing in Guru
Proceedings of the 4th ACM SIGPLAN workshop on programming languages meets program verification, pp.27-38
PLPV '10
01/19/2010
DOI: 10.1145/1707790.1707796
Abstract
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). We evaluate performance of the approach with two verified benchmarks, one involving mutable arrays, and another involving FIFO queues.
Details
- Title: Subtitle
- Resource typing in Guru
- Creators
- Aaron Stump - University of IowaEvan Austin - University of Kansas
- Resource Type
- Conference proceeding
- Publication Details
- Proceedings of the 4th ACM SIGPLAN workshop on programming languages meets program verification, pp.27-38
- Series
- PLPV '10
- DOI
- 10.1145/1707790.1707796
- Publisher
- ACM
- Language
- English
- Date published
- 01/19/2010
- Academic Unit
- Computer Science
- Record Identifier
- 9984259474702771
Metrics
13 Record Views