Incorporating Quotation and Evaluation into Church's Type Theory:
Syntax and Semantics

William M. Farmer

2016

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 and give several examples that illustrate the usefulness of
having quotation and evaluation in CTT_qe.  We do not give a proof
system for CTT_qe, but we do sketch what a proof system could look
like.