LiquidHaskell

Refinement Types via SMT and Predicate Abstraction

LiquidHaskell is a static verifier for Haskell, based on Liquid Types

Code

You can get LiquidHaskell here See the README for installation instructions. LiquidHaskell is an active research project that is still rough around the edges. In particular

  • A modest subset of the language is currently supported (monads recently included!…)

  • Error reporting is rather primitive

Constructive Feedback, or better yet, patches, additions and pull requests are extremely welcome.

Mailing List

If you have questions or comments, please send mail to the users mailing list

Papers

To learn about the theory behind Liquid Types, I recommend reading first the PLDI 2008 paper and then the ESOP 2013 paper. Alternatively, one lazy weekend, you could curl up with Pat Rondon’s Ph.D Dissertation

ML

Haskell

C

Talks

The following talks are good tutorial introductions to the techniques.

People

Liquid Types have been developed in the UCSD Programming Systems group by

Thanks

This work is funded by NSF grants CCF-0644361, CNS-0720802, CCF-0702603, and generous gifts from Microsoft Research.