类型理论的模块化构造
A modular construction of type theories
AI总结：
本文提出理论U，一个模块化类型理论构造，使得多个逻辑系统的证明可表达，并证明子理论符号使用对应子理论证明。
摘要：
lambda-Pi-演算模理论是一个逻辑框架，在其中许多类型系统可以被表示为理论。我们提出了这样一个理论，即理论U，其中多个逻辑系统的证明可以被表达。此外，我们识别出U的一个子理论对应于这些系统中的每一个，并证明当U中的一个证明仅使用某个子理论的符号时，它便是该子理论中的一个证明。
英文摘要：
The lambda-Pi-calculus modulo theory is a logical framework in which many type systems can be expressed as theories. We present such a theory, the theory U, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of U corresponding to each of these systems, and prove that, when a proof in U uses only symbols of a sub-theory, then it is a proof in that sub-theory.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
