The **Haskell Equational Reasoning Model-to-Implementation Tunnel** (HERMIT) is an NSF-funded project to improving the Applicability of Haskell-Hosted Semi-Formal Models to High Assurance Development.

In engineering practice, models are an essential part of understanding how to build complex systems. In this project, high-level models and efficient implementations of computer systems will be developed side-by-side under a single framework that bridges the gap between them using a high degree of automation. This is possible due to the use of a modern functional language for both the model and implementation, and the deployment of a new and powerful general-purpose and semi-automatic refinement technology.

The functional language Haskell has already enjoyed considerable success as a platform for high-level modeling of complex systems with its mathematical-style syntax, state-of-the-art type system, and powerful abstraction mechanisms. In this project, Haskell will be used to express a semi-formal model and an efficient implementation, taking the form of two distinct expressions of computation with the same mathematical foundation. The project develops tools and methodologies that use transformations like the worker/wrapper transformation to construct links between these models and implementations, lowering the cost of the development of high-assurance software and hardware components in application areas like security kernels and critical control systems. Lowering the cost of linking semi-formal specifications and models to real implementations will have considerable impact. For example, Evaluation Assurance Level (EAL) 5 and 6 of the Common Criteria call for semi-formal methods to construct such link, and this project addresses keys part of this requirement.

On Hackage: http://hackage.haskell.org/package/hermit

On Github: https://github.com/ku-fpg/hermit

- A. Farmer, C. Höner zu Siederdissen, and A. Gill. The hermit in the stream: Fusing stream fusion’s concatmap. In
*Proceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation*, PEPM ’14, pages 97–108, New York, NY, USA, 2014. ACM. ISBN 978-1-4503-2619-3. doi:`10.1145/2543728.2543736`

. URL http://doi.acm.org/10.1145/2543728.2543736. - M. D. Adams, A. Farmer, and J. P. Magalhães. Optimizing syb is easy! In
*Proceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation*, PEPM ’14, pages 71–82, New York, NY, USA, 2014. ACM. ISBN 978-1-4503-2619-3. doi:`10.1145/2543728.2543730`

. URL http://doi.acm.org/10.1145/2543728.2543730. - 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*, volume 8241 of*Lecture Notes in Computer Science*, pages 86–103, 2013. URL http://dx.doi.org/10.1007/978-3-642-41582-1_6. - 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, pages 1–12. ACM, 2012. ISBN 978-1-4503-1574-6. doi:`10.1145/2364506.2364508`

. URL http://doi.acm.org/10.1145/2364506.2364508.