EasyChair Proceedings in Computing
Search
Paper Information
Paper:Ramana Kumar
Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4
Title:Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4
Authors:Ramana Kumar
Keyphrases: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:Jasmin Christian Blanchette and Josef Urban (editors). PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Series:EasyChair Proceedings in Computing
Volume number:14
Pages:110-116
Editors:Jasmin Christian Blanchette and Josef Urban
BibTeX entry:
@inproceedings{PxTP2013:Challenges_in_Using_OpenTheory_to_Transport_Harrison_s_HOL_Model_from_HOL_Light_to_HOL4,
  author    = {Ramana Kumar},
  title     = {Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4},
  booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
  editor    = {Jasmin Christian Blanchette and Josef Urban},
  series    = {EasyChair Proceedings in Computing},
  volume    = {14},
  pages     = {110-116},
  year      = {2013},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2040-557X}}
Paper: