Document Type

Technical Report

Publication Date

2005-07-08

Filename

WUCSE-2005-32.pdf

DOI:

10.7936/K7RB730D

Technical Report Number

WUCSE-2005-32

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.

Comments

Permanent URL: http://dx.doi.org/10.7936/K7RB730D

Download

Share

COinS