Incorporating Quotation and Evaluation into Church's Type Theory

William M. Farmer

2018

Abstract

CTT_qe is a version of Church's type theory that includes quotation
and evaluation operators that are similar to quote and eval in the
Lisp programming language.  With quotation and evaluation it is
possible to reason in CTT_qe about the interplay of the syntax and
semantics of expressions and, as a result, to formalize syntax-based
mathematical algorithms.  We present the syntax and semantics of
CTT_qe as well as a proof system for CTT_qe.  The proof system is
shown to be sound for all formulas and complete for formulas that do
not contain evaluations.  We give several examples that illustrate the
usefulness of having quotation and evaluation in CTT_qe.