Simple Type Theory with Undefinedness, Quotation, and Evaluation

This paper presents a version of simple type theory called ${\cal Q}^{\rm uqe}_{0}$ that is based on ${\cal Q}_0$, the elegant formulation of Church's