Verifying Haskell's Rewrite Rules based on Polymorphic Rewriting Theory
summary
Presents a formal calculus System FRE — System Fω plus higher-order, polymorphic rewriting — and an automated checker ReCheck that verifies rewrite rules by proving termination (strong normalization) and local confluence via polymorphic higher-order unification and critical-pair analysis. Demonstrates automatic proofs for map fusion, append associativity and some monad laws on Core/Hackage code, and reports implementation limits: missing module resolution, built-in primitives, and the current need to assume the program is strongly normalizing (with a draft extension that relaxes this).
AI-written summary · about
chapters (13)
- 0:00GHC rewrite rules intro
- 3:56Correctness levels for rules
- 7:13Meaning preservation
- 9:23Formal correctness theorem
- 11:30Verifying append associativity
- 13:58Verifying map fusion
- 16:09Semantics for GHC rules
- 17:13System F Omega with rules
- 20:27Recheck plugin implementation
- 23:19Recheck experimental results
- 24:27Implementation challenges
- 26:57Future work and collaboration
- 29:32Q&A
related talks
23mHigher order Patterns in Rewrite Rules
28mFormalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
29mType Checking with Rewriting Rules
19mExtensible Metatheory Mechanization via Family Polymorphism
21mChecking Equivalence in a Non-strict Language
29mSemantic Transformation Framework for Rewriting Rules
16mA Hoare-Logic Style Refinement Types Formalisation
35mFlattening Meets Effects: A Surprising Connection