[Haskell-cafe] Tooling for equational reasoning in Haskell

[Paul Brauner]

Stepeval is what Christopher pointed to in his first email, but he said it
only works on a teeny weeny subset of Haskell.

On Tue Jan 27 2015 at 8:26:55 AM Sumit Sahrawat, Maths & Computing, IIT
(BHU) <sumit.sahrawat.apm13 at iitbhu.ac.in> wrote:

> 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"
>> https://bitbucket.org/naiman/nettyproject/overview
>> It is not specific to Haskell. It is a general-purpose calculational
>> proof assistant.
>>
>> 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
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>
>
>
> --
> Regards
>
> Sumit Sahrawat
>  _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20150127/98f281e2/attachment.html>