Liquid Types: Type Refinement via Predicate Abstraction

Patrick Rondon and Ranjit Jhala
September 18, 2007

Predicate abstraction and ML type inference are two well-known program analyses with very complementary strengths. The former is a technique for inferring precise, local, path-sensitive properties of base data values like integers but which is thwarted by complex data types and higher-order functions. The latter elegantly captures coarse properties of recursive data types and higher order functions. We present \emph{Liquid Types}, a system that synergistically combines the complementary strengths of predicate abstraction and ML type inference to yield an algorithm for statically inferring properties well beyond the scope of either technique. We have implemented liquid type inference for $\lang$, an extension of the $\lambda$-calculus with recursive types and ML style polymorphism. We present examples showing how liquid types can be used to statically prove the absence of divide-by-zero errors, out-of-bounds array access errors, and pattern match errors, with little to no user annotation.

How to view this document

The authors of these documents have submitted their reports to this technical report series for the purpose of non-commercial dissemination of scientific work. The reports are copyrighted by the authors, and their existence in electronic format does not imply that the authors have relinquished any rights. You may copy a report for scholarly, non-commercial purposes, such as research or instruction, provided that you agree to respect the author's copyright. For information concerning the use of this document for other than research or instructional purposes, contact the authors. Other information concerning this technical report series can be obtained from the Computer Science and Engineering Department at the University of California at San Diego,

[ Search ]

This server operates at UCSD Computer Science and Engineering.
Send email to