Project Page Index Table of Contents
  • Axiomatic Assumptions
    • Functional Extensionality
  • Syntax
    • Atoms
    • Applicative Head
    • Type Functions
    • Free Variables
  • Semantics
    • Compatibility Properties
    • Normality Characterisation
    • Inversion Lemmas
  • Equational Theory
    • Compatibility Properties
    • Injectivity Properties
    • Disjointness Properties
    • Huet Definition
  • Simple Typing
    • Preservation
  • Order Typing
    • Order of Types
    • Order Typing
    • Preservation Order Typing
  • Terms Extension
    • Typing
    • Semantics
    • Big Arrow
    • List Abstraction and Application
    • Substitutions and Renaming
    • Compatibility Properties
    • Equivalence Inversions
    • Normality
    • List Operators Typing
    • Utilities
  • Confluence
  • Weak Normalisation
    • Logical Relations
    • Semantic Soundness
    • Termination
  • Evaluator
    • Step Indexed Interpreter
    • Evaluator
  • Higher-Order Unification
    • Normalisation
  • System Unification
    • Normalisation
  • Nth-Order Unification
    • Nth-Order System Unification
    • Nth-Order Normalisation
  • Enumerability
    • Terms, Types and Contexts
    • Typing Proofs
    • Substitutions
    • Higher-Order Unification
  • PCP and MPCP
  • Third-Order Encoding
    • Encoding Typing
    • Encoding Properities
      • Reduction
      • Substitution
      • Injectivity
  • Simplified Reduction
    • Reduction Function
    • Forward Direction
    • Backward Direction
  • Huet Reduction
    • Reduction Function
    • Forward Direction
    • Backward Direction
  • Higher-Order Motivation
    • Church Numerals
    • Characteristic Equation
    • Diophantine Equations Encoding
    • Reduction Function
    • Equivalences
    • Forward Direction
    • Backward Direction
  • Second-Order Realisation
    • Goldfarb Numerals
    • Encoding
    • Characteristic Equation
    • Variables
    • Diophantine Equations Encoding
    • Reduction Function
    • Equivalences
      • Multiplication
    • Forward Direction
    • Backward Direction
    • Multiplication Motivation
  • First-Order Unification
    • Singlepoint Substitution
    • Lambda-Freeness
    • Simplified First-Order Unification
      • Term Decompositon
      • Unification Relation
      • Computability
      • Soundness
      • Completeness
      • Algorithm Equations
    • Full First-Order Unification
  • Conservativity
    • Constant Operations
    • Inhabiting Types
    • Conservativity
    • Consequences
  • Constants
    • Adding Constants
    • Removing Constants
    • Goldfarb sharp
    • Retyping
  • Enumerability from Conservativity
    • Nth-Order Unification
    • System Unification
    • Nth-Order System Unification
Generated by coqdoc and improved with CoqdocJS