Refined typechecking with Stardust

PLPV 2007 (Freiburg, Germany, October 2007)

Jana Dunfield

Abstract

We present Stardust, an implementation of a type system for a subset of ML with type refinements, intersection types, and union types, enabling programmers to legibly specify certain classes of program invariants that are verified at compile time. This is the first implementation of unrestricted intersection and union types in a mainstream functional programming setting, as well as the first implementation of a system with both datasort and index refinements. The system—with the assistance of external constraint solvers—supports integer, Boolean and dimensional index refinements; we apply both value refinements (to check red-black tree invariants) and invaluable refinements (to check dimensional consistency). While typechecking with intersection and union types is intrinsically complex, our experience so far suggests that it can be practical in many instances.

Reader’s guide

Morally, this paper is a proper subset of chapters 6 ("Implementation") and 7 ("Index domains") of my dissertation.

Slides

Workshop version* (August 2007)

* This PDF is one page longer than the published version, in which I had to shrink the references to meet the page limit. (It's bad policy to count references against page limits, but so it goes.)

Example code

BibTeX entry

@InProceedings{Dunfield07:Stardust,
  author =     {Jana Dunfield},
  title =      {Refined typechecking with {Stardust}},
  booktitle =  {Programming Languages meets Program Verification (PLPV '07)},
  month =      oct,
  year =       2007,
  editor =     {A. Stump and H. Xi},
  address =    {Freiburg, Germany}
}
  

all papers * related papers
J. Dunfield