Christina Kirk, Aart Middeldorp
Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2025), pp. 156-170, 2025.
pdf 
doi:10.1145/3703595.3705881
Abstract
We report on the formalization of a sufficient condition for confluence of first-order left-linear rewrite systems within the proof assistant Isabelle/HOL. This criterion, originally proposed by Okui (1998), is based on simultaneous critical pairs, which finitely represent peaks consisting of a multi-step and a normal step. It properly subsumes the formalized result on development-closed critical pairs.
BibTex
@inproceedings{CKAM-CPP25, author = "Christina Kirk and Aart Middeldorp", title = "Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems", booktitle = "Proceedings of the 14th International {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs", editors = "Kathrin Stark and Amin Timany and Sandrine Blazy and Nicolas Tabareau", publisher = "ACM", pages = "156--170", doi = "10.1145/3703595.3705881", year = 2025}