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";;