Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
summary
Formalizes parallel critical pairs and the Gramlich/Toyama/Shintani–Hirokawa criteria in Isabelle, replacing a messy position-based notion with a context-based definition that yields a simple recursive PCP algorithm. Implements a renaming-aware unifier called mgRen unification that returns lists of substitutions and proves soundness/completeness lemmas. Integrates these into the CeTA certifier, extends all criteria to commutation, and raises the number of certifiable Hakusan proofs by about 20 (from 159 to 179).
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:42Certification meaning
- 3:11Confluence and commutation
- 6:27Parallel critical pairs matter
- 9:25Formalizing parallel critical pairs
- 16:40Unification with renaming
- 21:23Critical pairs via contexts
- 23:55Key lemma for local peaks
- 25:25Results and competition impact
- 26:51Q&A
- 29:00Q&A
- 30:27Closing
related talks
28mFormalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
17mFormalizing Determinacy of Concurrent Revisions
31mAn Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
15mCompiling with Continuations, Correctly
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
58mA New Perspective on Commutativity in Verification
21mChecking Equivalence in a Non-strict Language