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 条
  • [31] A polynomial algorithm for uniqueness of normal forms of linear shallow term rewrite systems
    Zinn, Julian
    Verma, Rakesh M.
    APPLICABLE ALGEBRA IN ENGINEERING COMMUNICATION AND COMPUTING, 2010, 21 (06) : 459 - 485
  • [32] Synchronized Tree Languages for Reachability in Non-right-linear Term Rewrite Systems
    Boichut, Yohan
    Pelletier, Vivien
    Rety, Pierre
    REWRITING LOGIC AND ITS APPLICATIONS, WRLA 2016, 2016, 9942 : 64 - 81
  • [33] PARTIAL TYPE ASSIGNMENT IN LEFT LINEAR APPLICATIVE TERM REWRITING-SYSTEMS - THEORY, APPLICATIONS AND IMPLEMENTATION
    VANBAKEL, S
    SMETSERS, S
    BROCK, S
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 581 : 300 - 321
  • [34] DEVELOPMENT AND EVALUATION OF ELECTRICALLY ACTUATED ABDOMINAL LEFT-VENTRICULAR ASSIST SYSTEMS FOR LONG-TERM USE
    FUQUA, JM
    IGO, SR
    HIBBS, CW
    POIRIER, VL
    CHAMBERS, JA
    CLAY, WC
    MCGEE, MG
    TURNER, SA
    NORMAN, JC
    JOURNAL OF THORACIC AND CARDIOVASCULAR SURGERY, 1981, 81 (05): : 718 - 726
  • [35] HUMAN LEFT-VENTRICULAR (LV) APEX ORIENTATION - AN IMPORTANT VARIABLE IN THE DEVELOPMENT OF LONG-TERM (GREATER-THAN 2 YR) LEFT-VENTRICULAR ASSIST SYSTEMS
    TURNER, SA
    MCGEE, MG
    EDELMAN, SK
    FUQUA, JM
    NORMAN, JC
    CLINICAL RESEARCH, 1980, 28 (04): : A716 - A716
1234