Liquid Haskell

Liquid Haskell
Original authorsNiki Vazou, Eric Seidel
Ranjit Jhala
Release2014; 12 years ago (2014)
Stable release
0.9.14.1 / May 7, 2026; 5 months ago (2026-05-07)
Written inHaskell
Available inEnglish
TypeFormal program verifier
LicenseBSD 3-clause
Websiteucsd-progsys.github.io/liquidhaskell
Repositorygithub.com/ucsd-progsys/liquidhaskell

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

See also

References

  1. ↑ "Release v0.9.14.1". GitHub. May 7, 2026. Retrieved 2026-09-23.
  2. ↑ Vazou, Niki (2016). Liquid Haskell: Haskell as a theorem prover (Thesis). University of California.
  3. ↑ 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.

Further reading