Theorem proving for all: equational reasoning in liquid Haskell (functional pearl)

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

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).

Citation

Vazou, N., Breitner, J., Kunkel, R., Van Horn, D., & Hutton, G. (2018, September). Theorem proving for all: equational reasoning in liquid Haskell (functional pearl). Presented at ICFP '18: 23nd ACM SIGPLAN International Conference on Functional Programming, St. Louis MO USA

• Presentation Conference Type: Edited Proceedings
• Conference Name: ICFP '18: 23nd ACM SIGPLAN International Conference on Functional Programming
• Start Date: Sep 27, 2018
• End Date: Sep 28, 2018
• Acceptance Date: Aug 14, 2018
• Online Publication Date: Sep 17, 2018
• Publication Date: Sep 17, 2018
• Deposit Date: Aug 16, 2018
• Publicly Available Date: Nov 18, 2018
• Publisher: Association for Computing Machinery (ACM)
• Peer Reviewed: Peer Reviewed
• Pages: 132-144
• Book Title: Haskell 2018: Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell
• ISBN: 9781450358354
• DOI: https://doi.org/10.1145/3242744.3242756
• Keywords: Liquid Haskell; Theorem proving; Haskell; Equational reasoning; Program optimization
• Public URL: https://nottingham-repository.worktribe.com/output/1035977
• 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
• Contract Date: Aug 16, 2018