Liquid Haskell: Verification with Refinement Types
summary
Liquid Haskell is a GHC plugin that checks refinement types and lets Haskell programs carry SMT-checkable predicates; it proves safe indexing and non-division by zero, runs inside the build, and offers an automation called PLLE proof by logical evaluation to hide routine equational steps. The project proves real meta properties — a noninterference model needed 5.5k lines of proof — and a formal soundness development is about a 10k-line soundness proof while the implementation is ~400k LOC and sees ~five unsoundness reports per year.
AI-written summary · about
chapters (10)
- 0:00Refinement types intro
- 1:52Liquid Haskell as GHC plugin
- 5:47Deep verification with proofs
- 15:55How refinement types work
- 19:25Refinement types expressiveness
- 24:42Domain-specific properties
- 25:05Generality across languages
- 27:12Soundness of refinement types
- 30:25Practicality vs. soundness
- 33:38Future vision
related talks
46mRefinement Types from Light to Deep Verification
58mLiquidHaskell: Liquid Types for Haskell
21mRefinement Type Refutations
23mUsability Barriers for Liquid Types (Summary of Published Work)
29mExplicit Refinement Types
16mA Hoare-Logic Style Refinement Types Formalisation
01h 05mAll the Languages Together
21mVerifying term graph optimizations using Isabelle/HOL