Journal article
A language-based approach to functionally correct imperative programming
SIGPLAN notices, Vol.40(9), pp.268-279
09/12/2005
DOI: 10.1145/1090189.1086400
Abstract
In this paper a language-based approach to functionally correct imperative programming is proposed. The approach is based on a programming language called RSP1, which combines dependent types, general recursion, and imperative features in a type-safe way, while preserving decidability of type checking. The methodology used is that of internal verification, where programs manipulate programmer-supplied proofs explicitly as data. The fundamental technical idea of RSP1 is to identify problematic operations as impure, and keep them out of dependent types. The resulting language is powerful enough to verify statically non-trivial properties of imperative and functional programs. The paper presents the ideas through the examples of statically verified merge sort, statically verified imperative binary search trees, and statically verified directed acyclic graphs.
Details
- Title: Subtitle
- A language-based approach to functionally correct imperative programming
- Creators
- Edwin Westbrook - Washington University in Saint LouisAaron Stump - Washington University in Saint LouisIan Wehrman - Washington University in Saint Louis
- Resource Type
- Journal article
- Publication Details
- SIGPLAN notices, Vol.40(9), pp.268-279
- DOI
- 10.1145/1090189.1086400
- ISSN
- 0362-1340
- eISSN
- 1558-1160
- Language
- English
- Date published
- 09/12/2005
- Academic Unit
- Computer Science
- Record Identifier
- 9984259417402771
Metrics
12 Record Views