Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Transporting Theorems about Typeability in LF Across Schematically Defined Contexts

Chase Johnson, Gopalan Nadathur

TL;DR

The paper addresses transporting theorems about LF-typeability across schematically defined contexts by introducing context-schema subsumption within the logic $\mathcal{L}_{LF}$ and a sound transportation proof rule. It formalizes context expressions, block schemas, and substitutions, proving that validity is preserved under suitable schema substitutions and renamings. The authors implement the rule in the Adelfa proof assistant and demonstrate practical reasoning benefits, including lifting library results to richer context schemas. This work advances modular, context-aware reasoning about LF specifications and provides automated tooling to support such transport across derivations. The approach enhances formal verification tasks that rely on higher-order abstract syntax and dependent typing in LF-based encodings.

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.

Transporting Theorems about Typeability in LF Across Schematically Defined Contexts

TL;DR

The paper addresses transporting theorems about LF-typeability across schematically defined contexts by introducing context-schema subsumption within the logic and a sound transportation proof rule. It formalizes context expressions, block schemas, and substitutions, proving that validity is preserved under suitable schema substitutions and renamings. The authors implement the rule in the Adelfa proof assistant and demonstrate practical reasoning benefits, including lifting library results to richer context schemas. This work advances modular, context-aware reasoning about LF specifications and provides automated tooling to support such transport across derivations. The approach enhances formal verification tasks that rely on higher-order abstract syntax and dependent typing in LF-based encodings.

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 , 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 . 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.

Paper Structure

This paper contains 16 sections, 13 theorems, 8 equations, 10 figures.

Table of Contents

  1. Introduction
  2. The Edinburgh Logical Framework
  3. LF Syntax and Formation Judgements
  4. Subordination and Context Redundancies
  5. Reasoning About LF Judgements
  6. Formulas in the Logic and their Meaning
  7. Proving the Validity of Formulas
  8. Context Schema Subsumption
  9. Context Expression Subsumption
  10. Variants of a Block Schema
  11. Subsumption for Context Schemas
  12. Transporting Theorems Across Context Schemas
  13. Validity Under an Ill-formed Context Variable Substitution
  14. A Proof Rule for Transporting Theorems
  15. Using the Proof Rule in Reasoning
  16. ...and 1 more sections

Key Result

proposition 1

Let $\Gamma$ and $\Gamma'$ be contexts and let $A$ be a type such that $\vdash_{\Sigma} \Gamma\ \hbox{\tt ctx}$ and $\Gamma\vert^{\preceq}_{A} = \Gamma'$. Then the following are true:

Figures (10)

  • Figure 1: The Syntax of LF Expressions
  • Figure 2: Encoding Sizes of Untyped Lambda Terms
  • Figure 3: Well-formedness Judgements for Block and Context Schemas
  • Figure 4: Instantiating a Context Schema
  • Figure 5: Subordination of a Type by a Formula
  • ...and 5 more figures

Theorems & Definitions (20)

  • definition 1
  • proposition 1
  • definition 2
  • definition 3
  • definition 4
  • lemma 1
  • theorem 1
  • definition 5
  • theorem 2
  • theorem 3
  • ...and 10 more