Liquid Haskell
Original author(s) | Niki Vazou, Eric Seidel Ranjit Jhala |
---|---|
Initial release | 2014; 10 years ago (2014) |
Stable release | 0.9.2.5 / October 18, 2023; 8 months ago (2023-10-18) |
Repository | github |
Written in | Haskell |
Available in | English |
Type | Formal program verifier |
License | BSD 3-clause |
Website | ucsd-progsys |
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
- ^ Vazou, Niki (2016). Liquid Haskell: Haskell as a theorem prover (Thesis). University of California.
- ^ 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
- v
- t
- e
Haskell programming
Implementations (features) |
| ||||||||
---|---|---|---|---|---|---|---|---|---|
Libraries |
| ||||||||
Package managers |
| ||||||||
Windowing systems | |||||||||
Web frameworks |
| ||||||||
![](http://upload.wikimedia.org/wikipedia/en/thumb/4/4d/Logo_of_the_Haskell_programming_language.svg/100px-Logo_of_the_Haskell_programming_language.svg.png)
Eponym |
---|
- Arvind
- Lennart Augustsson
- Richard Bird
- Jeremy Gibbons
- Andrew D. Gordon
- Paul Hudak
- John Hughes
- John Launchbury
- John MacFarlane
- Simon Marlow
- Conor McBride
- Erik Meijer
- Simon Peyton Jones
- David Roundy
- Simon Thompson
- Philip Wadler
![](http://upload.wikimedia.org/wikipedia/commons/thumb/8/89/Symbol_book_class2.svg/16px-Symbol_book_class2.svg.png)
![](http://upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/16px-Symbol_category_class.svg.png)
![](http://upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/16px-Symbol_category_class.svg.png)
![]() | This formal methods-related article is a stub. You can help Wikipedia by expanding it. |
- v
- t
- e
![]() | This free and open-source software article is a stub. You can help Wikipedia by expanding it. |
- v
- t
- e