We are interested in algorithms that manipulate mathematical expressions in mathematically meaningful ways. Expressions are syntactic, but most logics do not allow one to discuss syntax. CTTqe is a version of Church’s type theory that includes quotation and evaluation operators, akin to quote and eval in the Lisp programming language. Since the HOL logic is also a version of Church’s type theory, we decided to add quotation and evaluation to HOL to demonstrate the implementability of CTTqe and the benefits of having quotation and evaluation in a proof assistant. The resulting system is called HOL. Here we document the design of HOL and the challenges that needed to be overcome. The resulting implementation is freely available.
CITATION STYLE
Carette, J., Farmer, W. M., & Laskowski, P. (2018). HOL Light QE. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10895 LNCS, pp. 215–234). Springer Verlag. https://doi.org/10.1007/978-3-319-94821-8_13
Mendeley helps you to discover research relevant for your work.