DecSyn.Autosubst2.core

• • Functor Instances

DecSyn.Autosubst2.syntax

DecSyn.Autosubst2.unscoped

• Autosubst Header for Unnamed Syntax
  • Primitives of the Sigma Calculus.
  • Type Class Instances for Notation
  • Proofs for the substitution primitives.
  • Generic lifting of an allfv predicate
  • Notations for unscoped syntax
  • Tactics for unscoped syntax

DecSyn.admissible

• Typing rules that are admissible

DecSyn.algorithmic

• Definition of Coquand's algorithm and its correctness
  • Properties about weak-head reduction
  • Coquand's algorithm for equalities
  • Coquand's algorithm extended with subtyping

DecSyn.common

• Some common structures shared by most parts of the development
  • The lookup relation for the typing context
  • Definitions of canonical (ishf) and weak-head neutral (ishne) forms
  • Definition of weak-head reduction
  • Bove-Capretta domains for equalities
  • Bove-Capretta domains for subtyping
  • A computable version of HRed.R

DecSyn.conv_dec

• The Top-level definition of the decision procedure

DecSyn.cosn

• A more relaxed set of terms where -postponement holds

DecSyn.executable

• Computable equality and subtyping
  • Computable algorithmic equality
  • Computable algorithmic subtyping

DecSyn.executable_correct

• Equivalence between the computable functions and the inductive specifications
  • Soundness of the computable equality w.r.t the inductive spec
  • Completeness of the computable equality w.r.t the inductive spec
  • Soundness of the computable subtyping w.r.t the inductive spec
  • Completeness of the computable subtyping w.r.t the inductive spec

DecSyn.fp_red

• Definitions and properties of untyped relations
  • Parallel eta-reduction
  • The inductive characterization of strong normalization
  • beta-reduction
  • Parallel beta-reduction
  • Restrictive parallel eta-reduction
  • The abstract signature that is sufficient for eta-postponement to hold
  • Proof of eta-postponement parameterized by an abstract predicate P
  • eta-reduction
  • betaeta-reduction
  • Leftmost-outermost beta-reduction
  • betaeta-joinability
  • One-step reductionless subtyping
  • Untyped subtyping

DecSyn.logrel

• Logical predicate and "semantic" soundness
  • The declarative signature of the logical predicate
  • A signature containing the facts we'd like to derive from the logical predicate
  • Proofs of the properties about the logical predicate from the abstract interface LogRel
  • An implementation of the LogRel signature with an explicit recursor InterpExt
  • Instantiating LogRelFacts with the concrete implementation LogRelImpl
  • Semantic typing defined in terms of the logical predicate
  • Structural properties about closing substitutions and semantic typing
  • Semantic typing rules

DecSyn.preservation

• Proof of preservation/subject reduction

DecSyn.soundness

• The fundamental theorem

DecSyn.structural

• Structural rules for the typing relation (renaming, substitution)

DecSyn.typing

• Typing specification