Journal article
HOL Light QE
Abstract
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 …
Authors
Carette J; Farmer WM; Laskowski P
Journal
Lecture Notes in Computer Science, Vol. 10895, , pp. 215–234
Publisher
Springer Nature
Publication Date
2018
DOI
10.1007/978-3-319-94821-8_13
ISSN
0302-9743