Skip to main content

Introducing the Haskell equational reasoning assistant

DOI 10.1145/1159842.1159856 dblp BibTeX

Abstract

We introduce the new, improved version of the Haskell Equational Reasoning Assistant, which consists of an Ajax application for rewriting Haskell fragments in their context, and an API for scripting non-trivial rewrites.

Related papers

The HERMIT in the machine: a plugin for the interactive transformation of GHC core language programs Haskell 2012
Reasoning with the HERMIT: tool support for equational reasoning on GHC core programs Haskell 2015
Speculate: discovering conditional equations and inequalities about black-box functions by reasoning from test results Haskell 2017
Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant JFP 2022
Pattern Matching with Abstract Data Types JFP 1993
How to prove decidability of equational theories with second-order computation analyser SOL JFP 2019
A compositional theory for STM Haskell Haskell 2009
Total Haskell is reasonable Coq CPP 2018