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/ |