A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems

被引：3
|
作者：
Kohl, Christina [1 ]
Middeldorp, Aart [1 ]
机构：
[1] Univ Innsbruck, Dept Comp Sci, Innsbruck, Austria
来源：
PROCEEDINGS OF THE 12TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2023 | 2023年
基金：
奥地利科学基金会;
关键词：
formalization; term rewriting; confluence; DECREASING DIAGRAMS; CONFLUENCE;
D O I：
10.1145/3573105.3575667
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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
引用
收藏
页码：197 / 210
页数：14
相关论文
共 35 条
1234