Automating Equational Proofs in Dirac Notation

被引：0
|
作者：
Xu, Yingte [1 ]
Barthe, Gilles [2 ]
Zhou, Li [3 ]
机构：
[1] Germany and Institute of Software, MPI-SP, Chinese Academy of Sciences, China
[2] Germany and IMDEA Software Institute, MPI-SP, Spain
[3] Institute of Software, Chinese Academy of Sciences, China
来源：
Proceedings of the ACM on Programming Languages | 2025年 / 9卷
关键词：
This research was supported by the National Key R&D Program of China under Grant No. 2023YFA1009403 and by Deutsche Forschungsgemeinschaft (DFG; German Research Foundation) as part of the Excellence Strategy of the German Federal and State Governments - EXC 2092 CASA - 390781972;
D O I：
10.1145/3704878
中图分类号：
学科分类号：
摘要：
77
引用
收藏
相关论文
共 50 条
  • [11] Automating Termination Proofs for CHR
    Pilozzi, Paolo
    De Schreye, Danny
    LOGIC PROGRAMMING, 2009, 5649 : 504 - 508
  • [12] Automating proofs in category theory
    Kozen, Dexter
    Kreitz, Christoph
    Richter, Eva
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 392 - 407
  • [13] Automating the Search for Elegant Proofs
    Larry Wos
    Journal of Automated Reasoning, 1998, 21 : 135 - 175
  • [14] A Core Calculus for Equational Proofs of Cryptographic Protocols
    Gancher, Joshua
    Sojakova, Kristina
    Fan, Xiong
    Shi, Elaine
    Morrisett, Greg
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2023, 7 (POPL): : 866 - 892
  • [15] Equational Security Proofs of Oblivious Transfer Protocols
    Li, Baiyu
    Micciancio, Daniele
    PUBLIC-KEY CRYPTOGRAPHY - PKC 2018, PT I, 2018, 10769 : 527 - 553
  • [16] EQUATIONAL INFERENCE, CANONICAL PROOFS, AND PROOF ORDERINGS
    BACHMAIR, L
    DERSHOWITZ, N
    JOURNAL OF THE ACM, 1994, 41 (02) : 236 - 276
  • [17] On automating diagrammatic proofs of arithmetic arguments
    Jamnik M.
    Bundy A.
    Green I.
    Journal of Logic, Language and Information, 1999, 8 (3) : 297 - 321
  • [18] Decision Procedures for Automating Termination Proofs
    Piskac, Ruzica
    Wies, Thomas
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2011, 6538 : 371 - +
  • [19] Automating algebraic proofs in algebraic logic
    Hsiang, Jieh
    Wasilewska, Anita
    Fundamenta Informaticae, 1996, 28 (1-2) : 129 - 140
  • [20] Automating Formal Proofs for Reactive Systems
    Ricketts, Daniel
    Robert, Valentin
    Jang, Dongseok
    Tatlock, Zachary
    Lerner, Sorin
    ACM SIGPLAN NOTICES, 2014, 49 (06) : 452 - 462
12345