Liquid Haskell

Liquid Haskell
Original authors	Niki Vazou, Eric Seidel Ranjit Jhala
Initial release	2014;11 years ago (2014)
Stable release	0.9.12.2 / March 22, 2025;8 months ago (2025-03-22)
Repository	github.com/ucsd-progsys/liquidhaskell
Written in	Haskell
Available in	English
Type	Formal program verifier
License	BSD 3-clause
Website	ucsd-progsys.github.io/liquidhaskell

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

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

• 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).
• Diatchki, Iavor (2015). "Improving Haskell types with SMT". Proceedings of the 8th ACM SIGPLAN Symposium on Haskell - Haskell 2015. ACM. pp. 1–10. doi:10.1145/2804302.2804307. ISBN   9781450338080. S2CID   16429107.

External links

• "Liquid Haskell - HaskellWiki". wiki.haskell.org. Retrieved 31 March 2019.
• Liquid Haskell on GitHub