HOL LIGHT QE

HOL Light QE is a proof assistant that implements the logic CTT_qe, a version of Church's type theory with quotation and evaluation. CTT_qe is presented in the paper "Incorporating Quotation and Evaluation into Church's Type Theory" which is available at:

https://doi.org/10.1016/j.ic.2018.03.001 (journal version) http://imps.mcmaster.ca/doc/qe-in-church.pdf (preprint version)

HOL Light QE is described in the paper "HOL Light QE" available at:

http://imps.mcmaster.ca/doc/hol-light-qe.pdf

The root of the system's GitHub code repository is:

https://github.com/JacquesCarette/hol-light-qe

HOL Light QE is a modification of the HOL Light proof assistant (which is described in the file README-hol-light). Like HOL Light, it is written in Objective CAML (OCaml) and uses the toplevel from OCaml as its front end. HOL Light QE is, roughly speaking, HOL Light plus quotation and evaluation operators. It is a conservative extension of HOL Light that works exactly like HOL Light when expressions have no quotations or evaluations.

To run HOL Light QE, execute the following commands in the HOL Light QE top-level directory named hol-light-qe:

1) install opam 2) opam init --comp 4.03.0
3) opam install "camlp5=6.16" 4) opam config env 5) cd hol-light-qe 6) make 7) run ocaml via
ocaml -I camlp5 -where camlp5o.cma
8) #use "hol.ml";;

use "Constructions/epsilon.ml";;

 #use "Constructions/pseudoquotation.ml";;
 #use "Constructions/QuotationTactics.ml";;