SeCaV: A Sequent Calculus Verifier in Isabelle/HOL

被引：0

作者：

From, Asta Halkjær ^{[1
]}

Jacobsen, Frederik Krogsdal ^{[1
]}

Villadsen, Jørgen ^{[1
]}

机构：

[1] DTU Compute, Department of Applied Mathematics and Computer Science, Technical University of Denmark, Denmark

来源：

Electronic Proceedings in Theoretical Computer Science, EPTCS | 2022年 / 357卷

关键词：

D O I：

16th Logical and Semantic Frameworks with Applications, LSFA 2021

中图分类号：

学科分类号：

摘要：

Differentiation (calculus) - Calculations - Formal logic - Theorem proving

引用

页码：38 / 55

共 50 条

[41] Stateful Protocol Composition in Isabelle/HOL
Hess, Andreas V.
Modersheim, Sebastian A.
Brucker, Achim D.
ACM TRANSACTIONS ON PRIVACY AND SECURITY, 2023, 26 (03)
[42] Weak alternating automata in Isabelle/HOL
Merz, S
THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 424 - 441
[43] Bounded Model Generation for Isabelle/HOL
Weber, Tjark
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 125 (03) : 103 - 116
[44] Formalizing provable anonymity in Isabelle/HOL
Li, Yongjian
Pang, Jun
FORMAL ASPECTS OF COMPUTING, 2015, 27 (02) : 255 - 282
[45] Formalizing rewriting introduction on Isabelle/HOL
Kimura Y.
Aoto T.
Computer Software, 2020, 37 (02) : 104 - 119
[46] Algebras for Program Correctness in Isabelle/HOL
Armstrong, Alasdair
Gomes, Victor Bf
Struth, Georg
RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMICS 2014), 2014, 8428 : 49 - 64
[47] Lyndon Words Formalized in Isabelle/HOL
Holub, Stepan
Starosta, Stepan
DEVELOPMENTS IN LANGUAGE THEORY, DLT 2021, 2021, 12811 : 217 - 228
[48] Reconstructing veriT Proofs in Isabelle/HOL
Fleury, Mathias
Schurr, Hans-Jorg
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2019, (301): : 36 - 50
[49] Algebraically Closed Fields in Isabelle/HOL
De Vilhena, Paulo Emilio
Paulson, Lawrence C.
AUTOMATED REASONING, PT II, 2020, 12167 : 204 - 220
[50] Verifying Secure Speculation in Isabelle/HOL
Griffin, Matt
Dongol, Brijesh
FORMAL METHODS, FM 2021, 2021, 13047 : 43 - 60