EasyChair logo

Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4

Ramana Kumar

Paper Information

TitleChallenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4
AuthorsRamana Kumar
Keywords:OpenTheory, proof transport, HOL4, HOL Light, higher-order logic, simple type theory
Abstract:OpenTheory is being used for the first time (in work to be described at ITP 2013) as a tool in a larger project, as opposed to in an example demonstrating OpenTheory's capability. The tool works, demonstrating its viability. But it does not work completely smoothly, because the use case is somewhat at odds with OpenTheory's primary design goals. In this extended abstract, we explore the tensions between the goals that OpenTheory-like systems might have, and question the relative importance of various kinds of use. My hope is that describing issues arising from work in progress will stimulate fruitful discussion relevant to the development of proof exchange systems.
Volume:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Pages:110-116
Editors:Jasmin Christian Blanchette and Josef Urban
BibTeX entry:
@inproceedings{EasyChair:224,
  author    = {Ramana Kumar},
  title     = {Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4},
  booktitle = {PxTP 2013},
  editor    = {Jasmin Christian Blanchette and Josef Urban},
  series    = {EPiC Series},
  volume    = {14},
  pages     = {110-116},
  year      = {2013},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2040-557X},
}
Paper:PDF