Research Repository

See what's under the surface

Theorem proving for all: equational reasoning in Liquid Haskell (Functional Pearl)

Vazou, Niki; Breitner, Joachim; Kunkel, Rose; van Horn, David; Hutton, Graham

Authors

Niki Vazou

Joachim Breitner

Rose Kunkel

David van Horn

Abstract

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 Hutton’s textbook can be recast as proofs in Haskell (spoiler: they look essentially the same).

Start Date Sep 27, 2018
Publication Date Sep 27, 2018
Publisher Association for Computing Machinery (ACM)
Pages 132-144
Book Title Proceedings of the 11th ACM SIGPLAN Haskell Symposium (Haskell '18)
ISBN 9781450358354
Institution Citation VAZOU, N., BREITNER, J., KUNKEL, R., VAN HORN, D., & HUTTON, G. (2018). Theorem proving for all: equational reasoning in Liquid Haskell (Functional Pearl). In Proceedings of the 11th ACM SIGPLAN Haskell Symposium (Haskell '18), 132-144. doi:10.1145/3242744.3242756
DOI https://doi.org/10.1145/3242744.3242756
Keywords Liquid Haskell; Theorem proving; Haskell; Equational reasoning; Program optimization
Publisher URL https://dl.acm.org/citation.cfm?id=3242756
Related Public URLs https://icfp18.sigplan.org/track/haskellsymp-2018-papers#event-overview
Additional Information Published in: Haskell 2018 Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell. Pages 132-144

St. Louis, MO, USA — September 27 - 28, 2018
ACM New York, NY, USA ©2018
ISBN: 978-1-4503-5835-4 doi: 10.1145/3242744.3242756

Files




You might also like


Downloadable Citations