A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
Christina Kohl and Aart Middeldorp
Proceedings of the 12th ACM SIGPLAN International Conference on Certified
Programs and Proofs (CPP 2023), pp. 197 – 210, 2023
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 Entry
@inproceedings{KM-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",
pages = "197--210",
doi = "10.1145/3573105.3575667",
year = 2023
}