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 条
  • [1] Importing HOL into Isabelle/HOL
    Obua, Steven
    Skalberg, Sebastian
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 298 - 302
  • [2] 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):
  • [3] Unifying Theories in Isabelle/HOL
    Feliachi, Abderrahmane
    Gaudel, Marie-Claude
    Wolff, Burkhart
    UNIFYING THEORIES OF PROGRAMMING, 2010, 6445 : 188 - +
  • [4] Random testing in Isabelle/HOL
    Berghofer, S
    Nipkow, T
    PROCEEDINGS OF THE SECOND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, 2004, : 230 - 239
  • [5] An Isabelle-Like Procedural Mode for HOL Light
    Papapanagiotou, Petros
    Fleuriot, Jacques
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, 2010, 6397 : 565 - 580
  • [6] A comparison of PVS and Isabelle/HOL
    Griffioen, D
    Huisman, M
    THEOREM PROVING IN HIGHER ORDER LOGICS, 1998, 1479 : 123 - 142
  • [7] Data Refinement in Isabelle/HOL
    Haftmann, Florian
    Krauss, Alexander
    Kuncar, Ondrej
    Nipkow, Tobias
    INTERACTIVE THEOREM PROVING, ITP 2013, 2013, 7998 : 100 - 115
  • [8] Nominal techniques in Isabelle/HOL
    Urban, Christian
    JOURNAL OF AUTOMATED REASONING, 2008, 40 (04) : 327 - 356
  • [9] From LCF to Isabelle/HOL
    Paulson, Lawrence C.
    Nipkow, Tobias
    Wenzel, Makarius
    FORMAL ASPECTS OF COMPUTING, 2019, 31 (06) : 675 - 698
  • [10] Linear Resources in Isabelle/HOL
    Smola, Filip
    Fleuriot, Jacques D.
    JOURNAL OF AUTOMATED REASONING, 2024, 68 (02)
12345