Refinement Types from Light to Deep Verification
summary
Shows a working Liquid Haskell plugin integrated with GHC that uses SMT-backed refinement types to prove light properties like safe indexing and no-division-by-zero automatically, and manual proofs (right identity, associativity, distributivity of reverse+append) via proof combinators, PLVE (proof by logical evaluation), and a rewrite-with tactic. Demonstrates a 10K-line mechanized proof encoding progress/preservation (soundness) of the model, notes good error messages for light checks, brittle messages for deep proofs, and remaining trusted-code-base soundness bugs.
AI-written summary · about
chapters (12)
- 0:00Refinement types intro
- 1:25Safe indexing with refinements
- 4:17Division by zero prevention
- 7:28Refinements vs dependent types
- 11:50Deep verification with Liquid Haskell
- 15:50Proof by logical evaluation
- 20:54Proving reverse and append
- 29:13Core principles of Liquid Haskell
- 33:00Refinement types expressiveness
- 36:33Soundness of refinement systems
- 39:25Soundness bugs and TCB
- 42:16Future of refinement types
related talks
34mLiquid Haskell: Verification with Refinement Types
29mExplicit Refinement Types
58mLiquidHaskell: Liquid Types for Haskell
21mRefinement Type Refutations
16mA Hoare-Logic Style Refinement Types Formalisation
23mUsability Barriers for Liquid Types (Summary of Published Work)
19mAutomated Verification of Fundamental Algebraic Laws
21mVerifying term graph optimizations using Isabelle/HOL