Automating Soundness Proofs

被引：3
|
作者：
van Weerdenburg, Muck [1 ]
机构：
[1] Eindhoven Univ Technol TU e, Dept Math & Comp Sci, Eindhoven, Netherlands
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2009年 / 229卷 / 04期
关键词：
structural operational semantics; axiomatisation; soundness; theorem proving;
D O I：
10.1016/j.entcs.2009.07.076
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
When developing a new language with semantics described by Structural Operational Semantics ( SOS), one often wants an axiomatisation of this language (w.r.t. to some equivalence) as well. We describe a method for automating the straightforward soundness proofs for the axioms of such an axiomatisation.
引用
收藏
页码：107 / 118
页数：12
相关论文
共 50 条
  • [1] Automating type soundness proofs via decision procedures and guided reductions
    Syme, D
    Gordon, AD
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, 2002, 2514 : 418 - 434
  • [2] REMARKS ON SOUNDNESS OF PROOFS
    BURMESTER, MVD
    DESMEDT, YG
    ELECTRONICS LETTERS, 1989, 25 (22) : 1509 - 1511
  • [3] Automating Proofs
    Edwards, Chris
    COMMUNICATIONS OF THE ACM, 2016, 59 (04) : 13 - 15
  • [4] Compositional Soundness Proofs of Abstract Interpreters
    Keidel, Sven
    Poulsen, Casper Bach
    Erdweg, Sebastian
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES, 2018,
  • [5] Compositional Soundness Proofs of Abstract Interpreters
    Keidel, Sven
    Poulsen, Casper Bach
    Erdweg, Sebastian
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2
  • [6] On Soundness Notions for Interactive Oracle Proofs
    Block, Alexander R.
    Garreta, Albert
    Tiwari, Pratyush Ranjan
    Zajac, Michal
    JOURNAL OF CRYPTOLOGY, 2025, 38 (01)
  • [7] Soundness and Completeness Proofs by Coinductive Methods
    Blanchette, Jasmin Christian
    Popescu, Andrei
    Traytel, Dmitriy
    JOURNAL OF AUTOMATED REASONING, 2017, 58 (01) : 149 - 179
  • [8] Soundness and Completeness Proofs by Coinductive Methods
    Jasmin Christian Blanchette
    Andrei Popescu
    Dmitriy Traytel
    Journal of Automated Reasoning, 2017, 58 : 149 - 179
  • [9] Type Soundness Proofs with Definitional Interpreters
    Amin, Nada
    Rompf, Tiark
    ACM SIGPLAN NOTICES, 2017, 52 (01) : 666 - 679
  • [10] Type soundness proofs with definitional interpreters
    Amin N.
    Rompf T.
    2017, Association for Computing Machinery (52): : 666 - 679
12345