학술논문

Certified HLints with Isabelle/HOLCF-Prelude
Document Type
Working Paper
Source
Subject
Computer Science - Logic in Computer Science
Language
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.
Comment: 1st International Workshop on Haskell And Rewriting Techniques, HART 2013, 5 pages