A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
Christina Kohl, Aart MiddeldorpProceedings 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
@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
}