Liquid Haskell

Liquid Haskell is a program verifier for Haskell which allows developers to specify correctness properties by using refinement types.[1][2] Properties are verified using an SMTLIB2-compliant SMT solver, such as the Z3 Theorem Prover.

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

  • Vazou, Niki. 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.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.