Loading...
Please wait, while we are loading the content...
Similar Documents
Practical Refinement-Type Checking (1997)
| Content Provider | CiteSeerX |
|---|---|
| Author | Pfenning, Frank Davies, Rowan |
| Abstract | Refinement types allow many more properties of programs to be expressed and statically checked than conventional type systems. We present a practical algorithm for refinement-type checking in a -calculus enriched with refinement-type annotations. We prove that our basic algorithm is sound and complete, and show that every term which has a refinement type can be annotated as required by our algorithm. Our positive experience with an implementation of an extension of this algorithm to the full core language of Standard ML demonstrates that refinement types can be a practical program development tool in a realistic programming language. The required refinement type definitions and annotations are not much of a burden and serve as formal, machine-checked explanations of code invariants which otherwise would remain implicit. 1 Introduction The advantages of statically-typed programming languages are well known, and have been described many times (e.g. see [Car97]). However, conventional ty... |
| File Format | |
| Publisher Date | 1997-01-01 |
| Access Restriction | Open |
| Subject Keyword | Realistic Programming Language Practical Program Development Tool Practical Algorithm Standard Ml Conventional Type System Code Invariant Basic Algorithm Statically-typed Programming Language Required Refinement Type Definition Machine-checked Explanation Refinement-type Annotation Refinement-type Checking Refinement Type Conventional Ty Many Time Positive Experience Full Core Language |
| Content Type | Text |
