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 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 mail the users mailing list

Tutorials

• Short
• Long

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
• Tech Report

Haskell

• Refinement Types For Haskell, ICFP 2014
• LiquidHaskell in the Real World, Haskell 2014
• Abstract Refinement Types, ESOP 2013

ML

• 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

C

• Low-level Liquid Types, POPL 2010
• Deterministic Parallelism With Liquid Effects, PLDI 2012
• Verifying C With Liquid Types, CAV 2012

Talks

The following talks are good tutorial introductions to the techniques.

• Tutorial at VMCAI
• Tutorial at CAV

People

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

• Alexander Bakst
• Ranjit Jhala
• Ming Kawaguchi
• Patrick Rondon
• Eric Seidel
• Michael Smith
• Anish Tondwalkar
• Chris Tetreault
• Niki Vazou

Thanks

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

---