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.

BibTeX

@inproceedings{JBBHNMCS-HART13,
  author      = "Joachim Breitner and Brian Huffman and Neil Mitchell and Christian Sternagel",
  title       = "Certified HLints with Isabelle/HOLCF-Prelude",
  booktitle   = "Proceedings of the 1st International Workshop on Haskell and Rewriting Techniques",
  year        = 2013
}