nn COMPUTER SCIENCE TECHNICAL REPORT ABSTRACTS
CMU-CS-07-129
Computer Science Department
School of Computer Science, Carnegie Mellon University


CMU-CS-07-129

A Unified System of Type Refinements

Jana Clara Dunfield

August 2007
Ph.D. Thesis

CMU-CS-07-129.pdf


Keywords: Type refinements, intersection types, union types, datasort refinements, index refinements, dimension types

Types 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.

284 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu