Loading...
Please wait, while we are loading the content...
Similar Documents
A language-based approach to functionally correct imperative programming (2005).
| Content Provider | CiteSeerX |
|---|---|
| Author | Stump, Aaron Wehrman, Ian Westbrook, Edwin |
| 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. |
| File Format | |
| Publisher Date | 2005-01-01 |
| Access Restriction | Open |
| Subject Keyword | Type Checking Dependent Type Language-based Approach Imperative Programming Merge Sort Programmer-supplied Proof Functional Program Resulting Language Verified Imperative Binary Search Tree Functionally Correct Imperative Programming Non-trivial Property Problematic Operation Programming Language Type-safe Way Acyclic Graph General Recursion Internal Verification Imperative Feature Fundamental Technical Idea |
| Content Type | Text |
| Resource Type | Article |
