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卷
关键词：
Compilation and indexing terms; Copyright 2024 Elsevier Inc;
D O I：
16th Logical and Semantic Frameworks with Applications, LSFA 2021
中图分类号：
学科分类号：
摘要：
Differentiation (calculus) - Calculations - Formal logic - Theorem proving
引用
收藏
页码：38 / 55
相关论文
共 50 条
  • [1] SeCaV: A Sequent Calculus Verifier in Isabelle/HOL
    From, Asta Halkjaer
    Jacobsen, Frederik Krogsdal
    Villadsen, Jorgen
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2022, (357): : 38 - 55
  • [2] A sequent calculus for first-order logic formalized in Isabelle/HOL
    From, Asta Halkjaer
    Schlichtkrull, Anders
    Villadsen, Jorgen
    JOURNAL OF LOGIC AND COMPUTATION, 2023, 33 (04) : 818 - 836
  • [3] Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
    From, Asta Halkjaer
    Jacobsen, Frederik Krogsdal
    JOURNAL OF AUTOMATED REASONING, 2024, 68 (03)
  • [4] An Isabelle/HOL Formalization of the SCL(FOL) Calculus
    Bromberger, Martin
    Desharnais, Martin
    Weidenbach, Christoph
    AUTOMATED DEDUCTION, CADE 29, 2023, 14132 : 116 - 133
  • [5] Proving the soundness of a Java']Java bytecode verifier specification in Isabelle/HOL
    Pusch, C
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 1999, 1579 : 89 - 103
  • [6] Importing HOL into Isabelle/HOL
    Obua, Steven
    Skalberg, Sebastian
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 298 - 302
  • [7] An interpretation of Isabelle/HOL in HOL Light
    McLaughlin, Sean
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 192 - 204
  • [8] A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
    Röckl, C
    Hirschkoff, D
    JOURNAL OF FUNCTIONAL PROGRAMMING, 2003, 13 : 415 - 451
  • [9] Safety and Conservativity of Definitions in HOL and Isabelle/HOL
    Kuncar, Ondrej
    Popescu, Andrei
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2 (POPL):
  • [10] Unifying Theories in Isabelle/HOL
    Feliachi, Abderrahmane
    Gaudel, Marie-Claude
    Wolff, Burkhart
    UNIFYING THEORIES OF PROGRAMMING, 2010, 6445 : 188 - +
12345