Jana Clara Dunfield

A Unified System of Type Refinements Degree Type: Ph.D. in Computer Science
Advisor(s): Frank Pfenning
Graduated: August 2007

Abstract:

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.

Thesis Committee:
Frank Pfenning (Chair)
Jonathan Aldrich
Robert Harper
Benjamin Pierce (University of Pennsylvania)

Jeannette Wing, Head, Computer Science Department
Randy Bryant, Dean, School of Computer Science

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