LiquidHaskell

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

• 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

Haskell

• Abstract Refinement Types, ESOP 2013

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
• Niki Vazou

Thanks

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