[Haskell-cafe] Tooling for equational reasoning in Haskell
Alberto G. Corona
agocorona at gmail.com
Wed Jan 28 08:28:41 UTC 2015
There is a interpreter of Haskell written in Maude:
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
>> 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 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
>> Sumit Sahrawat
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe