Thesis oral details: Practical refinement-type checking (Rowan Davies)
Title: Practical refinement-type checking
Speaker: Rowan Davies
Time: 1pm Friday February 11, 2005
Place: Wean Hall 4623
Thesis committee: Frank Pfenning, Chair
Alex Aiken, Stanford University
Thesis summary: www.cs.cmu.edu/~rowan/thesis-summary.pdf (14 pages)
Software development is a complex and error prone task. Programming languages
with strong static type systems assist programmers by capturing and checking
the fundamental structure of programs in a very intuitive way. Given this
success, it is natural to ask: can we capture and check more of the structure
In this work I consider a new approach called refinement-type checking
that allows many common program properties to be captured and checked. This
approach builds on the strength of the type system of a language by adding the
ability to specify refinements of each type. Such "refinement types" have been
considered previously, and following previous work I focus on refinements that
include subtyping and a form of intersection types.
Central to my approach is the use of a bidirectional checking algorithm.
This does not attempt to infer refinements for some expressions, such as
functions, but only checks them against refinements. This avoids some
difficulties encountered in previous work, and requires that the programmer
annotate their program with some of the intended refinements, but the required
annotations appear to be very reasonable. Further, they document properties in
a way that is natural, precise, easy to read, and reliable.
I demonstrate the practicality of my approach by showing that it can be
used to design a refinement-type checker for a widely-used language with a
strong type system: Standard ML. This requires two main technical
developments. Firstly, I present a new variant of intersection types that
achieve soundness in the presence of call-by-value effects by incorporating a
value restriction. Secondly, I present a practical approach to incorporating
recursive refinements of ML datatypes, including a pragmatic method for
checking the sequential pattern matching construct of ML.
I also report the results of some experiments with my implementation of
refinement-type checking for SML. These indicate that refinement-type checking
is a practical method for capturing and checking properties of real code.