LiquidHaskell is a static verifier for Haskell, based on Liquid Types
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.
If you have questions or comments, please send mail to the users mailing list
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:
- Refinement Types For Haskell, ICFP 2014
- LiquidHaskell in the Real World, Haskell 2014
- Abstract Refinement Types, ESOP 2013
- Liquid Types, PLDI 2008
- Type-based Data Structure Verification, PLDI 2009
- Dsolve: Safety Verification via Liquid Types, CAV 2010
- HMC: Verifying Functional Programs with Abstract Interpreters, CAV 2011
- Low-level Liquid Types, POPL 2010
- Deterministic Parallelism With Liquid Effects, PLDI 2012
- Verifying C With Liquid Types, CAV 2012
The following talks are good tutorial introductions to the techniques.
Liquid Types have been developed in the UCSD Programming Systems group by
This work is funded by NSF grants CCF-0644361, CNS-0720802, CCF-0702603, and generous gifts from Microsoft Research.