Rowan Davies

Practical Refinement-Type Checking Degree Type: Ph.D. in Computer Science
Advisor(s): Frank Pfenning
Graduated: May 2005

Abstract:

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 of programs?

In this dissertation I describe an 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. 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. 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 obtain 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 conclude by reporting the results of 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.

Thesis Committee:
Frank Pfenning (Chair)
Robert Harper
Peter Lee
John Reynolds
Alex Aiken (Stanford University)

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

Keywords:
Programming languages, type systems, intersection types, bidirectional checking, value restricted polymorphism, regular-tree types