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.
BSD LicenseTopics
Theories of HOLCF-Prelude
- HOLCF_Main
- Type_Classes
- Numeral_Cpo
- Data_Function
- Data_Bool
- Data_Tuple
- Data_Integer
- Data_List
- Data_Maybe
- Definedness
- List_Comprehension
- Num_Class
- HOLCF_Prelude
- Fibs
- Sieve_Primes
- GHC_Rewrite_Rules
- HLint