Liquid Haskell Explained

Liquid Haskell
Author:	Niki Vazou, Eric Seidel Ranjit Jhala
Latest Release Version:	0.9.2.5
Programming Language:	Haskell
Language:	English
Genre:	Formal program verifier
License:	BSD 3-clause

Liquid Haskell is a program verifier for the programming language Haskell which allows specifying correctness properties by using refinement types.^{[1] [2]} Properties are verified using a satisfiability modulo theories (SMT) solver which is SMTLIB2-compliant, such as the Z3 Theorem Prover.

See also

• Formal verification

References

• Löh . Andres . 2018 . Liquid Haskell Workshop . BOB 2018.
• Jhala . Ranjit . 2014 . Liquid Haskell . Boston Haskell User Group.

Further reading

• Vazou . Niki . 2018 . Liquid Haskell: Refinement Types for Haskell . The 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018) .
• Book: Diatchki, Iavor . 2015 . Proceedings of the 8th ACM SIGPLAN Symposium on Haskell - Haskell 2015 . 1–10 . Improving Haskell types with SMT . ACM . 10.1145/2804302.2804307 . 9781450338080 . 16429107.

External links

• Web site: Liquid Haskell - HaskellWiki . wiki.haskell.org . 31 March 2019.

Notes and References

1. Vazou . Niki . Liquid Haskell: Haskell as a theorem prover . University of California . 2016.
2. Vazou . Niki . Seidel . Eric . 2014 . Refinement types for Haskell . ACM . Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming . 269–282 . International Conference on Functional Programming . 10.1145/2692915.2628161.