Tools
Tools
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
|
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: |
|
||||
| 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 |
Views
Views per month over past year
Downloads
Downloads per month over past year
