Theorem proving for all: equational reasoning in Liquid Haskell
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 a...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
2018
|
| Online Access: | https://eprints.nottingham.ac.uk/54770/ |
| _version_ | 1848799072205406208 |
|---|---|
| author | Vazou, Niki Breitner, Joachim Kunkel, Rose Van Horn, David Hutton, Graham |
| author_facet | Vazou, Niki Breitner, Joachim Kunkel, Rose Van Horn, David Hutton, Graham |
| author_sort | Vazou, Niki |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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). |
| first_indexed | 2025-11-14T20:29:51Z |
| format | Article |
| id | nottingham-54770 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T20:29:51Z |
| publishDate | 2018 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-547702022-10-05T09:59:20Z https://eprints.nottingham.ac.uk/54770/ Theorem proving for all: equational reasoning in Liquid Haskell Vazou, Niki Breitner, Joachim Kunkel, Rose Van Horn, David Hutton, Graham 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). 2018-09-27 Article PeerReviewed application/pdf en https://eprints.nottingham.ac.uk/54770/1/tpfa.pdf Vazou, Niki, Breitner, Joachim, Kunkel, Rose, Van Horn, David and Hutton, Graham (2018) Theorem proving for all: equational reasoning in Liquid Haskell. |
| spellingShingle | Vazou, Niki Breitner, Joachim Kunkel, Rose Van Horn, David Hutton, Graham Theorem proving for all: equational reasoning in Liquid Haskell |
| title | Theorem proving for all: equational reasoning in Liquid Haskell |
| title_full | Theorem proving for all: equational reasoning in Liquid Haskell |
| title_fullStr | Theorem proving for all: equational reasoning in Liquid Haskell |
| title_full_unstemmed | Theorem proving for all: equational reasoning in Liquid Haskell |
| title_short | Theorem proving for all: equational reasoning in Liquid Haskell |
| title_sort | theorem proving for all: equational reasoning in liquid haskell |
| url | https://eprints.nottingham.ac.uk/54770/ |