Equational Reasoning Assistant (ERA)

ERA is a syntax manipulation tool that allows users to do equational reasoning on Haskell programs. It has a graphical interface, letting users point and click on expressions (or sub-expressions), and transform these expressions in well defined ways.

ERA comes with a large library of lemmas about Haskell prelude functions. When released, Era will also have a proof butler that will help with typesetting the proofs that the user has performed.

Developers: Andy Gill and John O'Donnell, for the CM Haskell Project
Contact:
Number of Users: 2
Number of Sites: 2
Line Count: ~7000 lines, ~30 Modules
In use: Since Feb 1995
Language: Haskell 1.3
Compilers: Any 1.3 Haskell compiler
Availability: Details about the current status of ERA may be found on the CM Haskell web page: http://www.dcs.gla.ac.uk/~andy/era.html
The first public release is due RSN.