HOL Light QE

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. $${\textsc {ctt}}_\mathrm{qe}$$ 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 $$\text {HOL}$$ logic is also a version of Church’s type theory, we decided to add quotation and evaluation to $$\text {HOL Light}$$ to demonstrate the implementability of $${\textsc {ctt}}_\mathrm{qe}$$ and the benefits of having quotation and evaluation in a proof assistant. The resulting system is called $$\text {HOL Light QE}$$. Here we document the design of $$\text {HOL Light QE}$$ and the challenges that needed to be overcome. The resulting implementation is freely available.