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

Publications

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