Liquid Proof Macros
summary
Liquid Proof Macros is an extensible metaprogramming framework that uses Template Haskell to generate Liquid Haskell proof terms via a tactic-like DSL, and it automates many inductive proofs by expanding macros, running Liquid Haskell, and pruning unnecessary steps. The implementation reduces handwritten proof size by about 57% on benchmarks, supplies an Auto proof-search that nests hints, and demonstrably works, but it is slow from repeated checker invocations and lacks polymorphism support and tight LH API integration.
AI-written summary · about
chapters (8)
- 0:00Introduction to Liquid Haskell
- 2:12The need for proof automation
- 3:32Working with proof macros
- 6:33Proof script examples
- 9:36Advanced usage and bottlenecks
- 12:46Evaluation and results
- 14:00Design strategy and takeaways
- 16:53Implementation and future work
related talks
24mGradual Liquid Type Inference
01h 22mHaskell for Everyday Programmers
34mHackett: a metaprogrammable Haskell
01h 07m50,000 Lines of LLM Haskell: What Broke, What Held, and Letting Go
50mTemplate Haskell, a case study in (in)stability
50mMaking Risk Decisions with Haskell at Scale
47mLogic Programming à la Carte
46mPainless software development with Haskell