Certified HLints with Isabelle/HOLCF-Prelude
Logic in Computer Science
2013-06-07 v1
Abstract
We present the HOLCF-Prelude, a formalization of a large part of Haskell's standard prelude in Isabelle/HOLCF. Applying this formalization to the hints suggested by HLint allows us to certify them formally.
Cite
@article{arxiv.1306.1340,
title = {Certified HLints with Isabelle/HOLCF-Prelude},
author = {Joachim Breitner and Brian Huffman and Neil Mitchell and Christian Sternagel},
journal= {arXiv preprint arXiv:1306.1340},
year = {2013}
}
Comments
1st International Workshop on Haskell And Rewriting Techniques, HART 2013, 5 pages