Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] new AFP entry: HOLCF-Prelude

view this post on Zulip 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: Apr 20 2024 at 08:16 UTC