Email Gateway (Aug 22 2022 at 15:47): Email Gateway (Aug 22 2022 at 15:47):From: Gerwin Klein <gerwin.klein@data61.csiro.au>
https://www.isa-afp.org/entries/HOLCF-Prelude.shtml
HOLCF-Prelude
by Joachim Breitner, Brian Huffman, Neil Mitchell, and Christian Sternagel
Abstract
The Isabelle/HOLCF-Prelude is a formalization of a large part of
Haskell's standard prelude in Isabelle/HOLCF. We use it to prove
the correctness of the Eratosthenes' Sieve, in its
self-referential implementation commonly used to showcase
Haskell's laziness; prove correctness of GHC's
"fold/build" rule and related rewrite rules; and certify a
number of hints suggested by HLint.
Enjoy!
Gerwin
Last updated: Nov 21 2024 at 12:39 UTC