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 条
  • [21] Algebraic Numbers in Isabelle/HOL
    Thiemann, Rene
    Yamada, Akihisa
    INTERACTIVE THEOREM PROVING (ITP 2016), 2016, 9807 : 391 - 408
  • [22] Liveness Reasoning with Isabelle/HOL
    Wang, Jinshuang
    Yang, Huabing
    Zhang, Xingyuan
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2009, 5674 : 485 - 499
  • [23] Hoare logics in Isabelle/HOL
    Nipkow, T
    PROOF AND SYSTEM-RELIABILITY, 2002, 62 : 341 - 367
  • [24] Comprehending Isabelle/HOL's Consistency
    Kuncar, Ondrej
    Popescu, Andrei
    PROGRAMMING LANGUAGES AND SYSTEMS (ESOP 2017): 26TH EUROPEAN SYMPOSIUM ON PROGRAMMING, 2017, 10201 : 724 - 749
  • [25] A Modular Formalization of Superposition in Isabelle/HOL
    Desharnais, Martin
    Toth, Balazs
    Waldmann, Uwe
    Blanchette, Jasmin
    Tourret, Sophie
    Leibniz International Proceedings in Informatics, LIPIcs, 309
  • [26] Fast Machine Words in Isabelle/HOL
    Lochbihler, Andreas
    INTERACTIVE THEOREM PROVING, ITP 2018, 2018, 10895 : 388 - 410
  • [27] Imperative functional programming with Isabelle/HOL
    Bulwahn, Lukas
    Krauss, Alexander
    Haftmann, Horian
    Erkoek, Levent
    Matthews, John
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2008, 5170 : 134 - +
  • [28] A Denotational Semantics of Solidity in Isabelle/HOL
    Marmsoler, Diego
    Brucker, Achim D.
    SOFTWARE ENGINEERING AND FORMAL METHODS (SEFM 2021), 2021, 13085 : 403 - 422
  • [29] Automating Free Logic in Isabelle/HOL
    Benzmueller, Christoph
    Scott, Dana
    MATHEMATICAL SOFTWARE, ICMS 2016, 2016, 9725 : 43 - 50
  • [30] Extracting a normalization algorithm in Isabelle/HOL
    Berghofer, S
    TYPES FOR PROOFS AND PROGRAMS, 2006, 3839 : 50 - 65
12345