Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell
summary
Mechanizes coinductive proofs inside Liquid Haskell by encoding coinduction two ways: indexed coinduction (use a natural-number index to reduce stream equality to equality of prefixes) and constructive coinduction (a guarded, constructor-based equality that enforces productivity). Demonstrates the pattern on map fusion and other stream/list properties, requires a take-lemma axiom to recover full equality, uses Liquid Haskell proof combinators, and successfully machine-checks 10 coinductive proofs with artifacts available.
AI-written summary · about
chapters (7)
- 0:00Introduction to stream proofs
- 2:10Liquid Haskell overview
- 3:33Inductive map fusion proof
- 7:11Challenges with co-induction
- 8:39Indexed equality approach
- 13:52Constructive equality approach
- 20:17Comparison and conclusion
related talks
24mGradual Liquid Type Inference
49mMaking sense of the Haskell type system
34mHaskell⁻¹: Automatic Function Inversion in Haskell
01h 22mHaskell for Everyday Programmers
51mGreek Classics: Lambda Calculus For Beginners
01h 02mHaskell for Java Programmers
38mRefactoring Recursion
59mKeynote: Dependently-Typed Haskell