将引用与求值纳入丘奇类型论

${\rm CTT}_{\rm qe}$ 是丘奇类型论的一个版本，包含类似于 Lisp 编程语言中 quote 和 eval 的引用(quotation)与求值(evaluation)算子。借助引用与求值，可以在 ${\rm CTT}_{\rm qe}$ 中对表达式的语法与语义之间的相互作用进行推理，从而形式化基于语法的数学算法。我们给出了 ${\rm CTT}_{\rm qe}$ 的语法和语义，以及针对 ${\rm CTT}_{\rm qe}$ 的一个证明系统。该证明系统被证明对所有公式可靠，且对不含求值的公式完备。我们提供了若干示例来说明在 ${\rm CTT}_{\rm qe}$ 中拥有引用与求值的实用性。