The Haskell Equational Reasoning Model-to-Implementation Tunnel (HERMIT)

The Haskell Equational Reasoning Model-to-Implementation Tunnel (HERMIT) is a GHC plugin that allows post-hoc transformations to be applied to Haskell programs, after compilation has started. HERMIT can be used for program-specific optimizations, domain-specific optimizations, or for constructing semi-formal assurance arguments.

Architecture

The HERMIT Package

• On Hackage: http://hackage.haskell.org/package/hermit
• On Github: https://github.com/ku-fpg/hermit

Publications

• 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.

• A. Farmer, HERMIT: Mechanized Reasoning during Compilation in the Glasgow Haskell Compiler. PhD thesis, The University of Kansas, April 2015.

• M. D. Adams, A. Farmer, and J. P. Magalhães, “Optimizing SYB Traversals Is Easy!,” Science of Computer Programming, vol. 112, Part 2, pp. 170 – 193, 2015. Selected and extended papers from Partial Evaluation and Program Manipulation 2014.

• A. Farmer, C. Höner zu Siederdissen, and A. Gill, “The HERMIT in the Stream,” in Proceedings of the 2014 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM ’14, ACM, 2014.

• M. D. Adams, A. Farmer, and J. P. Magalhães, “Optimizing SYB Is Easy!,” in Proceedings of the 2014 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM ’14, ACM, 2014. Won Best Paper Award.

• N. Sculthorpe, A. Farmer, and A. Gill, “The HERMIT in the tree: Mechanizing program transformations in the GHC core language,” in Proceedings of the 24th Symposium on Implementation and Application of Functional Languages, vol. 8241 of Lecture Notes in Computer Science, pp. 86–103, 2013.

• A. Farmer, A. Gill, E. Komp, and N. Sculthorpe, “The HERMIT in the machine: A plugin for the interactive transformation of GHC core language programs,” in Proceedings of the ACM SIGPLAN Haskell Symposium, Haskell ’12, pp. 1–12, ACM, 2012.