[Haskell-cafe] Tooling for equational reasoning in Haskell

[Alberto G. Corona]

There is a interpreter of Haskell written in Maude:

http://fsl.cs.illinois.edu/images/5/5f/Bennett-2006-tr.pdf

Which potentially can do it, since Maude is an specificiation language
based on rewriting logic.  It has no IO neither has syntactic sugar for
lists, type classes etc, But it is a different path to achieving this goal
if someone is interested in developing it further



2015-01-27 11:35 GMT+01:00 Paul Brauner <polux2001 at gmail.com>:

> 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
>>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>


-- 
Alberto.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20150128/f4cffc0c/attachment.html>