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

Farmer, A, Sculthorpe, N ORCID: https://orcid.org/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

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:	Number Type 10.1145/2887747.2804303 DOI
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
URI:	https://irep.ntu.ac.uk/id/eprint/27907

Actions (login required)

Edit View

Statistics

Views

Downloads