LiquidHaskell: Liquid Types for Haskell
summary
LiquidHaskell is a tool that brings automated, expressive refinement (liquid) types to Haskell to statically verify properties like totality, termination, memory safety and safe resource use without requiring manual proofs. It integrates specifications into Haskell code and runs verification automatically, and has been applied to over 10,000 lines of real-world Haskell.
AI-written summary · about
chapters (16)
- 0:00Intro
- 1:01Software bugs are everywhere
- 2:53Make bugs difficult to express
- 4:39Valid Values for takeWord16?
- 6:22Checks valid arguments, under facts.
- 13:25Example: Parsing UDP
- 21:16Expressiveness vs. Automation
- 25:13Functional Correctness
- 28:07Totality
- 30:43Termination
- 34:52Theorem Proving
- 38:01Parallelisation Equivalence
- 38:55Example: Parallel Sums
- 40:50Parallelization Equivalence
- 42:38Liquid Haskell
- 45:20Refinement Types in Soala
related talks
34mLiquid Haskell: Verification with Refinement Types
16mVerifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
46mRefinement Types from Light to Deep Verification
23mUsability Barriers for Liquid Types (Summary of Published Work)
21mRefinement Type Refutations
28mQuotient Polymorphism
20mFlux: Liquid Types for Rust
20mTowards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax