Liquid Haskell

Last updated
Liquid Haskell
Original author(s) Niki Vazou, Eric Seidel
Ranjit Jhala
Initial release2014;11 years ago (2014)
Stable release
0.9.2.5 / October 18, 2023;19 months ago (2023-10-18)
Repository github.com/ucsd-progsys/liquidhaskell
Written in Haskell
Available inEnglish
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.

Contents

See also

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.

Further reading


Free and open-source software logo (2009).svg

This free and open-source software article is a stub. You can help Wikipedia by expanding it.

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.