cl-banner

Certified HLints with Isabelle/HOLCF-Prelude

Joachim Breitner, Brian Huffman, Neil Mitchell, and Christian Sternagel

Proceedings of the 1st International Workshop on Haskell and Rewriting Techniques (HART 2013), 2013.

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.

 

  PDF  |    arXiv

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
}
Nach oben scrollen