An Introduction to Liquid Haskell

Ricardo Peña
(Universidad Complutense de Madrid)

This paper is a tutorial introducing the underlying technology and the use of the tool Liquid Haskell, a type-checker for the functional language Haskell that can help programmers to verify non-trivial properties of their programs with a low effort.

The first sections introduce the technology of Liquid Types by explaining its principles and summarizing how its type inference algorithm manages to prove properties. The remaining sections present a selection of Haskell examples and show the kind of properties that can be proved with the system.

In Alicia Villanueva: Proceedings XVI Jornadas sobre Programación y Lenguajes (PROLE 2016), Salamanca, Spain, 14-16th September 2016, Electronic Proceedings in Theoretical Computer Science 237, pp. 68–80.
Published: 11th January 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.237.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org