Abstract

All existing translations between proof assistants have been notoriously sluggy, resource-demanding, and do not scale to large developments, which has lead to the general perception that the whole approach is probably not practical. We aim to show that the observed inefficiencies are not inherent, but merely a deficiency of the existing implementations. We do so by providing a new implementation of a theory import from HOL Light to Isabelle/HOL, which achieves decent performance and scalability mostly by avoiding the mistakes of the past.

After some preprocessing, our tool can import large HOL Light developments faster than HOL Light processes them. Our main target and motivation is the Flyspeck development, which can be imported in a few hours on commodity hardware. We also provide mappings for most basic types present in the developments including lists, integers and real numbers.

This papers outlines some design considerations and presents a few of our extensive measurements, which reveal interesting insights in the low-level structure of larger proof developments.

BibTeX

@inproceedings{CKAK-ITP13,
  author      = "Cezary Kaliszyk and Alexander Krauss",
  title       = "Scalable {LCF}-style Proof Translation",
  booktitle   = "Proceedings of the 4th International Conference on
                 Interactive Theorem Proving",
  editor      = "Sandrine Blazy and Christine Paulin-Mohring and
                 David Pichardie",
  series      = "Lecture Notes in Computer Science",
  volume      = 7998,
  pages       = "51--66",
  publisher   = "Springer-Verlag",
  year        = 2013,
  doi         = "10.1007/978-3-642-39634-2_7"
}