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
相关论文
共 32 条
  • [1] [Anonymous], 1910, PRINCIPIA MATH, DOI DOI 10.1017/CBO9780511623585
  • [2] AVIGAD J, IN PRESS ACM T COMPU
  • [3] BALLARIN C, 2003, TYPES PROOFS PROGRAM
  • [4] Bertot Yves, 2004, TEXT THEORET COMP S, DOI 10.1007/978-3-662-07964-5
  • [5] BRUIJN NGD, 1980, H B CURRY ESSAYS COM, P589
  • [6] Constable R., 1986, Implementing Mathematics with the Nuprl Development System
  • [7] FELTY AP, 1997, SPRINGER VERALG LECT, P351
  • [8] GONTHIER G, 2005, COMPTUER CHECKED PRO
  • [9] GORDON MJC, 1993, NTRO HOL THEOREM PRO
  • [10] HAKES T, 2005, JORDAN CURVE THEOREM
1234