A. Farmer, N. Sculthorpe, and A. Gill, “Reasoning with the HERMIT: Tool support for equational reasoning on GHC Core programs,” in Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, (New York, NY, USA), pp. 23–34, ACM, 2015.

Links

• http://doi.acm.org/10.1145/2804302.2804303

• http://www.ittc.ku.edu/csdl/fpg/files/Farmer-15-HERMIT-reasoning.pdf

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.

BibTeX

@inproceedings{Farmer:15:HERMIT-reasoning,
  author = {Andrew Farmer and Neil Sculthorpe and Andy Gill},
  title = {Reasoning with the {HERMIT}: {T}ool Support for Equational Reasoning on {GHC} {C}ore Programs},
  booktitle = {Proceedings of the 8th ACM SIGPLAN Symposium on Haskell},
  series = {Haskell 2015},
  location = {Vancouver, BC, Canada},
  year = {2015},
  isbn = {978-1-4503-3808-0},
  location = {Vancouver, BC, Canada},
  pages = {23--34},
  numpages = {12},
  doi = {10.1145/2804302.2804303},
  acmid = {2804303},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {Equational Reasoning, HERMIT, Type Class Laws},
}

Disclaimer

This is the author’s version of the work. It is posted here for your personal use. Not for redistribution. The definitive version was published in Haskell 2015, and is available in the ACM Digital Library.

Case Studies

Download the case studies here: Reasoning with the HERMIT Case Studies

Instructions for installing HERMIT (cabal update ; cabal install hermit-1.0.0.0) and running the case studies can be found in the README file contained within the case study archive.