Reasoning with the HERMIT: tool support for equational reasoning on GHC core programs

Farmer, A., Sculthorpe, N. ORCID: 0000-0002-7244-0916 and Gill, A., 2015. Reasoning with the HERMIT: tool support for equational reasoning on GHC core programs. ACM SIGPLAN Notices, 50 (12), pp. 23-34. ISSN 0362-1340

PubSub5456_Sculthorpe.pdf - Post-print

Download (418kB) | Preview


A benefit of pure functional programming is that it encourages equational reasoning. However, the Haskell language has lacked direct tool support for such reasoning. Consequently, reasoning about Haskell programs is either performed manually, or in another language that does provide tool support (e.g. Agda or Coq).
HERMIT is a Haskell-specific toolkit designed to support equational reasoning and user-guided program transformation, and to do so as part of the GHC compilation pipeline. This paper describes HERMIT’s recently developed support for equational reasoning,
and presents two case studies of HERMIT usage: checking that type-class laws hold for specific instance declarations, and mechanising textbook equational reasoning.

Item Type: Journal article
Description: Special issue: "Haskell '15".
Publication Title: ACM SIGPLAN Notices
Creators: Farmer, A., Sculthorpe, N. and Gill, A.
Publisher: ACM (Association for Computing Machinery)
Date: December 2015
Volume: 50
Number: 12
ISSN: 0362-1340
Divisions: Schools > School of Science and Technology
Record created by: Jill Tomkinson
Date Added: 27 May 2016 15:56
Last Modified: 13 Oct 2017 13:18

Actions (login required)

Edit View Edit View


Views per month over past year


Downloads per month over past year