The Multiverse：证明助手的逻辑模块化
The Multiverse: Logical Modularity for Proof Assistants
摘要：
证明助手扮演着程序设计语言和逻辑系统的双重角色。作为程序设计语言，证明助手提供了标准的模块化机制，如一级函数，类型多态性和模块。然而，作为逻辑系统，模块性是缺乏的，这是可以理解的：不兼容的推理原则-例如身份证明的唯一性和唯一性-在给定的开发中使用时，即使它们似乎局限于不同的模块，也会间接导致逻辑不一致。在证明助手中缺乏逻辑模块性也阻碍了采用更丰富的编程结构，比如效果。我们提出了多重宇宙，一个一般的类型理论的方法，赋予证明助手与逻辑模块化。多元宇宙由多个宇宙层次结构组成，这些层次结构静态地描述了可用于定义给定类型的术语的推理原则和效果。我们确定了充分的条件，这种结构模块化，以确保不兼容的原则不干涉，并在必要时，本地限制依赖消除的权力。这种可扩展的方法概括了Coq证明助手中对命题排序的特殊处理。我们通过描述包含Coq式命题，吉尔伯特等人的严格命题，Pédrot和Tabareau的例外类型论，以及逻辑的一般公理扩展。
英文摘要：
Proof assistants play a dual role as programming languages and logical systems. As programming languages, proof assistants offer standard modularity mechanisms such as first-class functions, type polymorphism and modules. As logical systems, however, modularity is lacking, and understandably so: incompatible reasoning principles -- such as univalence and uniqueness of identity proofs -- can indirectly lead to logical inconsistency when used in a given development, even when they appear to be confined to different modules. The lack of logical modularity in proof assistants also hinders the adoption of richer programming constructs, such as effects. We propose the multiverse, a general type-theoretic approach to endow proof assistants with logical modularity. The multiverse consists of multiple universe hierarchies that statically describe the reasoning principles and effects available to define a term at a given type. We identify sufficient conditions for this structuring to modularly ensure that incompatible principles do not interfere, and to locally restrict the power of dependent elimination when necessary. This extensible approach generalizes the ad-hoc treatment of the sort of propositions in the Coq proof assistant. We illustrate the power of the multiverse by describing the inclusion of Coq-style propositions, the strict propositions of Gilbert et al., the exceptional type theory of Pédrot and Tabareau, and general axiomatic extensions of the logic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
