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
                       Robert Harper
                       Peter Lee 
                       John Reynolds
                       Alex Aiken, Stanford University 

Thesis summary: www.cs.cmu.edu/~rowan/thesis-summary.pdf (14 pages)

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 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.