Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Fri 28 Sep 2018 15:30 - 15:59 at Illinois Central - Session 7 Chair(s): Simon Marlow

Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manually on paper, or mechanised in a theorem prover. This article shows how equational reasoning can be performed directly and seamlessly within Haskell itself, and be checked using Liquid Haskell. In particular, language learners — to whom external theorem provers are out of reach — can benefit from having their proofs mechanically checked. Concretely, we show how the equational proofs and derivations from Graham’s textbook can be recast as proofs in Haskell (spoiler: they look essentially the same).

Fri 28 Sep
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

15:30 - 16:00: Session 7Haskell at Illinois Central
Chair(s): Simon MarlowFacebook
15:30 - 15:59
Talk
Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl)
Haskell
Niki VazouUniversity of Maryland, USA, Joachim BreitnerDFINITY Foundation, Rose KunkelUniversity of Maryland, USA, David Van HornUniversity of Maryland, USA, Graham HuttonUniversity of Nottingham, UK
DOI
15:59 - 16:00
Talk
Closing Statement
Haskell
Nicolas WuUniversity of Bristol, UK