📝 SummarXiv

Abstract

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.