Haskell Equational Reasoning Assistant

The Haskell Equational Reasoning Assistant

Functional programmers often appeal to equational reasoning to justify various decisions made in both design and implementation. This page introduces the Haskell Equational Reasoning Assistant (HERA), an architecture that provides both a GUI level and a batch level Haskell rewrite engine inside a single tool. The interactive interface is used to create and edit non-trivial translations that can be used to extend the batch level API; the batch level API can be used to implement powerful, context sensitive rewrites that can be provided to the interactive interface.

The Interactive Interface

Ajax applications use a web browser interface, and provide a dynamic interactive experience beyond traditional CGI scripts, with user interactions causing localized updates to the displayed web pages, rather than complete page reloads[2]. An Ajax engine implemented in Javascript turns user interactions into asynchronous HTTP requests, sending them to the Ajax-compliant web server. The engine then comprehends the responses to the asynchronous requests, and uses Javascript to redraw only the parts of the interface that need updating.

HERA is a classical Ajax application consisting of two components: a client-side Ajax engine running inside the browser customized for HERA; and a server-side Haskell application which provides the rewrite engine, and interacts with the Javascript Ajax engine via a simple web server, also written in Haskell.

There are three main panels in the interface:

...