标题： 在结构化定义的上下文中传输LF中的可类型性定理 显示英文标题

标题： Transporting Theorems about Typeability in LF Across Schematically Defined Contexts

摘要： 依赖类型lambda演算LF常被用作形式化对象系统规则描述的载体。 证明以这种方式编码的对象系统的属性需要对LF类型判断上的公式进行推理。 LF的一个重要特性是它支持绑定结构的高阶抽象语法表示。 当使用这种编码时，类型判断包括为绑定变量分配类型的上下文，因此公式必须允许对上下文进行量化。 这种量词的可能实例通常由模式描述所控制，这些描述也必须明确表达以便在推理中有效。 在实际的推理任务中，常常需要将涉及满足一种模式描述的上下文全称量化的定理转移到满足另一种描述的上下文中。 我们在此提供对此能力的逻辑论证。 为此，我们利用了逻辑$\mathcal{L}_{LF}$，该逻辑之前已被设计用于形式化LF规范的性质。 我们开发了一个传输证明规则，并证明其相对于$\mathcal{L}_{LF}$的语义是正确的。 这个证明规则的关键是一个上下文模式子类化的概念，它使用类型之间的从属关系作为确定相对于单个LF类型判断的上下文等价性的手段。 我们讨论了该规则在Adelfa证明助手中的集成及其在实际推理示例中的应用。 显示英文摘要

摘要： The dependently-typed lambda calculus LF is often used as a vehicle for formalizing rule-based descriptions of object systems. Proving properties of object systems encoded in this fashion requires reasoning about formulas over LF typing judgements. An important characteristic of LF is that it supports a higher-order abstract syntax representation of binding structure. When such an encoding is used, the typing judgements include contexts that assign types to bound variables and formulas must therefore allow for quantification over contexts. The possible instantiations of such quantifiers are usually governed by schematic descriptions that must also be made explicit for effectiveness in reasoning. In practical reasoning tasks, it is often necessary to transport theorems involving universal quantification over contexts satisfying one schematic description to those satisfying another description. We provide here a logical justification for this ability. Towards this end, we utilize the logic $\mathcal{L}_{LF}$, which has previously been designed for formalizing properties of LF specifications. We develop a transportation proof rule and show it to be sound relative to the semantics of $\mathcal{L}_{LF}$. Key to this proof rule is a notion of context schema subsumption that uses the subordination relation between types as a means for determining the equivalence of contexts relative to individual LF typing judgements. We discuss the incorporation of this rule into the Adelfa proof assistant and its use in actual reasoning examples.