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

[img]
Preview
Text
PubSub5456_Sculthorpe.pdf - Post-print

Download (418kB) | Preview

Abstract

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
Identifiers:
NumberType
10.1145/2887747.2804303DOI
Divisions: Schools > School of Science and Technology
Depositing User: Jill Tomkinson
Date Added: 27 May 2016 15:56
Last Modified: 13 Oct 2017 13:18
URI: http://irep.ntu.ac.uk/id/eprint/27907

Actions (login required)

Edit View Edit View

Views

Views per month over past year

Downloads

Downloads per month over past year