An interpretation of Isabelle/HOL in HOL Light

被引：0
|
作者：
McLaughlin, Sean [1 ]
机构：
[1] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA
来源：
AUTOMATED REASONING, PROCEEDINGS | 2006年 / 4130卷
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We define an interpretation of the Isabelle/HOL logic in HOL Light and its metalanguage, OCaml. Some aspects of the Isabelle logic are not representable directly in the HOL Light object logic. The interpretation thus takes the form of a set of elaboration rules, where features of the Isabelle logic that cannot be represented directly are elaborated to functors in OCaml. We demonstrate the effectiveness of the interpretation via an implementation, translating a significant part of the Isabelle standard library into HOL Light.
引用
收藏
页码：192 / 204
页数：13
相关论文
共 50 条
  • [41] Automatic Proof and Disproof in Isabelle/HOL
    Blanchette, Jasmin Christian
    Bulwahn, Lukas
    Nipkow, Tobias
    FRONTIERS OF COMBINING SYSTEMS, 2011, 6989 : 12 - 27
  • [42] Programming Language Semantics with Isabelle/HOL
    Martini, Alfio
    2013 2ND WORKSHOP-SCHOOL ON THEORETICAL COMPUTER SCIENCE (WEIT), 2013, : 14 - 21
  • [43] Formalization of Differential Privacy in Isabelle/HOL
    Sato, Tetsuya
    Minamide, Yasuhiko
    PROCEEDINGS OF THE 14TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2025, 2025, : 67 - 82
  • [44] Lyndon Words Formalized in Isabelle/HOL
    Holub, Stepan
    Starosta, Stepan
    DEVELOPMENTS IN LANGUAGE THEORY, DLT 2021, 2021, 12811 : 217 - 228
  • [45] Reconstructing veriT Proofs in Isabelle/HOL
    Fleury, Mathias
    Schurr, Hans-Jorg
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2019, (301): : 36 - 50
  • [46] Algebraically Closed Fields in Isabelle/HOL
    De Vilhena, Paulo Emilio
    Paulson, Lawrence C.
    AUTOMATED REASONING, PT II, 2020, 12167 : 204 - 220
  • [47] Certifying Dictionary Construction in Isabelle/HOL
    Hupel, Lars
    FUNDAMENTA INFORMATICAE, 2019, 170 (1-3) : 177 - 205
  • [48] Verifying Secure Speculation in Isabelle/HOL
    Griffin, Matt
    Dongol, Brijesh
    FORMAL METHODS, FM 2021, 2021, 13047 : 43 - 60
  • [49] Certified Quantum Computation in Isabelle/HOL
    Anthony Bordg
    Hanna Lachnitt
    Yijun He
    Journal of Automated Reasoning, 2021, 65 : 691 - 709
  • [50] Combination of Isabelle/HOL with automatic tools
    Tverdyshev, S
    FRONTIERS OF COMBINING SYSTEMS, PROCEEDINGS, 2005, 3717 : 302 - 309
12345