Project Page Index Table of Contents
    • Functor Instances
      • List Instance
      • Prod Instance
      • Option Instance
  • Autosubst Header for Unnamed Syntax
    • Primitives of the Sigma Calculus.
    • Type Class Instances for Notation
      • Type classes for renamings.
      • Type Classes for Substiution
      • Type Class for Variables
    • Proofs for the substitution primitives.
    • Generic lifting of an allfv predicate
    • Notations for unscoped syntax
    • Tactics for unscoped syntax
  • General Header Autosubst - Assumptions and Definitions
    • Axiomatic Assumptions
      • Functional Extensionality
      • Function Instance
  • Specification of HOL
    • Typing judgements
    • HOL deduction system
    • Typed HOL deduction system
  • Specification of EffHOL
    • Reduction and conversion
    • Reduction and conversion renaming lemmas
    • Reduction and conversion substitution lemmas
    • Typing judgements
    • Judgement weakening lemmas
    • Judgement renaming lemmas
    • Judgement substitution lemmas
    • Church-Rosser property
    • Subject reduction
    • EffHOL deduction system
  • Translation from HOL to EffHOL
    • Translation functions
    • Translation substitution lemmas
    • Translation well-formedness lemmas
    • Soundness theorem
  • Translation from EffHOL to HOL
    • Translation functions
    • Simple lemmas
    • Main result
  • Instantiation into System F_w
    • Specification of System F_w
    • Syntax components
    • Assumptions about reduction and conversion
    • Assumptions about substitution
    • Assumptions about typing judgements
    • Assumptions about deductions
    • Translation of types and preservation lemma
    • Translation of programs and preservation lemma
    • Translation of indices and preservation lemma
    • Translation of specifications and expressions and preservation lemmas
    • Soundness of translation of HOPL into F_w
    • Combined translation of HOL into F_w
Generated by coqdoc and improved with CoqdocJS