[Haskell-cafe] Tooling for equational reasoning in Haskell
Albert Y. C. Lai
trebla at vex.net
Mon Jan 26 22:47:08 UTC 2015
On 2015-01-18 06:46 PM, Christopher Done wrote:
> I quite enjoy doing equational reasoning to prove that my functions
> satisfy some laws, I like to type out each substitution step until I
> get back what I started with. The only trouble is that it's rather
> manual and possibly error prone.
> Is there any tooling anywhere out there that can take in a Haskell
> expression and reduce it by one step?
I suggest my friend Lev Naiman's proof assistant project "Netty"
It is not specific to Haskell. It is a general-purpose calculational
If you want to take a look at a paper, it's somewhere on his home page:
More information about the Haskell-Cafe