[Haskell-cafe] Tooling for equational reasoning in Haskell
Sumit Sahrawat, Maths & Computing, IIT (BHU)
sumit.sahrawat.apm13 at iitbhu.ac.in
Tue Jan 27 07:26:44 UTC 2015
I found https://github.com/bmillwood/stepeval, which evaluates expressions
step-by-step. It might be possible to modify it for equational reasoning.
On 27 January 2015 at 04:17, Albert Y. C. Lai <trebla at vex.net> wrote:
> 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 proof
> If you want to take a look at a paper, it's somewhere on his home page:
> http://www.cs.utoronto.ca/~naiman/ <http://www.cs.utoronto.ca/%7Enaiman/>
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe