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 条
  • [31] Verified Real Asymptotics in Isabelle/HOL
    Eberl, Manuel
    PROCEEDINGS OF THE 2019 ACM INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION (ISSAC '19), 2019, : 147 - 154
  • [32] On the mechanization of real analysis in Isabelle/HOL
    Fleuriot, JD
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 145 - 161
  • [33] Formalizing O notation in Isabelle/HOL
    Avigad, J
    Donnelly, K
    AUTOMATED REASONING, PROCEEDINGS, 2004, 3097 : 357 - 371
  • [34] Stateful Protocol Composition in Isabelle/HOL
    Hess, Andreas V.
    Modersheim, Sebastian A.
    Brucker, Achim D.
    ACM TRANSACTIONS ON PRIVACY AND SECURITY, 2023, 26 (03)
  • [35] Weak alternating automata in Isabelle/HOL
    Merz, S
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 424 - 441
  • [36] Bounded Model Generation for Isabelle/HOL
    Weber, Tjark
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 125 (03) : 103 - 116
  • [37] Formalizing provable anonymity in Isabelle/HOL
    Li, Yongjian
    Pang, Jun
    FORMAL ASPECTS OF COMPUTING, 2015, 27 (02) : 255 - 282
  • [38] Formalizing rewriting introduction on Isabelle/HOL
    Kimura Y.
    Aoto T.
    Computer Software, 2020, 37 (02) : 104 - 119
  • [39] 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
  • [40] Certified Quantum Computation in Isabelle/HOL
    Bordg, Anthony
    Lachnitt, Hanna
    He, Yijun
    JOURNAL OF AUTOMATED REASONING, 2021, 65 (05) : 691 - 709
12345