Christina Kohl, Aart Middeldorp
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023), pp. 197-210, 2023.
pdf 
doi:10.1145/3573105.3575667
Abstract
Several critical pair criteria are known that guarantee confluence of left-linear term rewrite systems. The correctness of most of these have been formalized in a proof assistant. An important exception has been the development closedness criterion of van Oostrom. Its proof requires a high level of understanding about overlapping redexes and descendants as well as several intermediate results related to these concepts. We present a formalization in the proof assistant Isabelle/HOL. The result has been integrated into the certifier CeTA.
BibTex
@inproceedings{CKAM-CPP23, author = "Christina Kohl and Aart Middeldorp", title = "A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems", booktitle = "Proceedings of the 12th International {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs", editors = "Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka and Steve Zdancewic", publisher = "ACM", pages = "197--210", doi = "10.1145/3573105.3575667", year = 2023}