Certified HLints with Isabelle/HOLCF-Prelude
classification
💻 cs.LO
keywords
formalizationholcf-preludeisabelleallowsapplyingcertifiedcertifyformally
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.