Abstract: HOL Zero is a basic theorem prover that aims to achieve the highest levels of reliability and trustworthiness through careful design and implementation of its core components. In this paper, we concentrate on its treatment of concrete syntax, explaining how it manages to avoid problems suffered in other HOL systems related to the parsing and pretty printing of HOL types, terms and theorems, with the goal of achieving well-behaved parsing/printing and Pollack-consistency. Included are an explanation of how Hindley-Milner type inference is adapted to cater for variable-variable overloading, and how terms are minimally annotated with types for unambiguous printing.
Download PDF: hzsyntax_itp2016.pdf
Reference: M.Adams. HOL Zero's Solutions for Pollack-Inconsistency. In Proceedings of the 7th International Conference on Interactive Theorem Proving, Volume 9807 of Lecture Notes in Computer Science, pages 20-35. Springer, 2016.