Jump to content

Liquid Haskell

From Wikipedia, the free encyclopedia

This is an old revision of this page, as edited by Ghettoblaster (talk | contribs) at 01:34, 22 December 2019. The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

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

External links