Theory Morphisms in Church’s Type Theory with Quotation and Evaluation

Abstract$${\textsc {ctt}}_\mathrm{qe}$$ is a version of Church’s type theory with global quotation and evaluation operators that is engineered to reason about the interplay of syntax and semantics and to formalize syntax-based mathematical algorithms. $${\textsc {ctt}}_\mathrm{uqe}$$ is a variant of $${\textsc {ctt}}_\mathrm{qe}$$ that admits undefined expressions, partial functions, and multiple base types of individuals. It is better suited …