AbstractTypes express properties of programs; typechecking is specification checking. However, the specifications expressed by types in conventional type systems are imprecise. Type refinements address this by allowing programmers to express more precise properties, while keeping typechecking decidable and practical. We present a system of type refinements that unifies and extends past work on datasort and index refinements. We provide unified mechanisms of definite types, such as intersections, and indefinite types, such as unions. Through our development of contextual typing annotations, the tridirectional rule, and let-normal typechecking, we achieve a type system that is expressive and practical, requiring no user input besides type annotations. We show that our implementation of the type system can check several data structure invariants, as well as dimension types (an instance of invaluable refinements), in a subset of Standard ML. |
Reader’s guideSome of this material appeared, tersely and sometimes erroneously, in earlier papers. Chapter 2 incorporates important corrections to the proofs in our* FOSSACS '03 paper. Chapter 3 is a relatively limited revision to our* tech report (itself an extended version of our POPL '04 paper). In addition, the final draft of my PLPV '07 paper was submitted before the thesis was finalized; it covers much of Chapters 6 and 7.* Co-authored with Frank Pfenning. |
@PhdThesis{DunfieldThesis,
author = {Jana Dunfield},
title = {A Unified System of Type Refinements},
school = {Carnegie Mellon University},
year = {2007},
month = aug,
note = {CMU-CS-07-129}
}