Re: [Haskell-cafe] Tooling for equational reasoning in Haskell

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 :

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) 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 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Regards

Sumit Sahrawat _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Alberto.