Certified HLints with Isabelle/HOLCF-Prelude
Joachim Breitner, Brian Huffman, Neil Mitchell, Christian, Sternagel
TL;DR
This paper introduces HOLCF-Prelude, a formalization of Haskell's standard prelude in Isabelle/HOLCF, enabling formal certification of hints suggested by HLint.
Contribution
It provides the first formalization of Haskell's prelude in Isabelle/HOLCF for certifying HLint suggestions.
Findings
Successfully formalized a large part of Haskell's prelude
Enabled formal certification of HLint hints
Demonstrated the applicability of Isabelle/HOLCF for Haskell verification
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Security and Verification in Computing · Formal Methods in Verification