Unifying Principles of Type Refinements

PhD thesis proposal

Jana Dunfield


Traditional static type systems in the Hindley-Milner style are a useful means of guaranteeing type safety, in the form of type preservation and progress theorems, and of broadly specifying properties of functions (such as taking integers to lists of integers). In order to allow programmers to express stronger properties through static typing, I propose to develop and implement a rich type system that combines and extends work on datasort refinements, index refinements, intersection, and union types, and to show that it can check many interesting properties of functional programs that are difficult or impossible to check in conventional static type systems. Due to the richness of the type system, full type inference is undecidable, so a certain amount of annotation will be necessary. I intend to focus on properties of algebraic datatypes, such as list length or the set of keys mapped by a binary search tree. The type system's soundness is maintained in the presence of effects, but the properties are not about state. However, many of the techniques developed may be applicable to stateful properties as well.

Thesis Committee

Frank Pfenning (chair)
Robert Harper
Jonathan Aldrich
Benjamin Pierce (University of Pennsylvania)

Version of December 2003

BibTeX entry

  author = "Jana Dunfield",
  title = "Unifying principles of type refinements",
  howpublished = "PhD thesis proposal, Carnegie Mellon University",
  year = "2004"

all papers * related papers
J. Dunfield