(...) How to turn (Liquid) Haskell into a theorem prover
summary
Claims a lightweight way to retro-fit theorem proving into Haskell by reflecting function definitions into output refinement types so their code becomes logic at call sites. Implemented in Liquid Haskell it uses an SMT backend to discharge implications, checks termination and case coverage, and proves concrete properties like associativity of append and equivalence of MapReduce-based and sequential sums on Haskell’s parallel runtime. The method unfolds reflected functions exactly once at uses, requires user-written proof code in Haskell, and is decidable and predictable.
AI-written summary · about
chapters (6)
related talks
01h 44mAn Introduction to Natural Deduction
22mA Certifying Proof Assistant for Synthetic Mathematics in Lean
35mProof Theory Impressionism: Blurring the Curry-Howard Line
41mWar Time Proofs and Futuristic Programs
58mThe Next Great Functional Programming Language
01h 04mThe Leibniz Library and Applied Propositions as Types
01h 08mLean: Machine-Checked Mathematics and Verified Programming, Past and Future
19mVelvet: A Multi-Modal Verifier for Effectful Programs