Project Page Index Table of Contents
  • Chpater 4 : Pure Sigma Calculus.
    • Syntax and Reduction
      • Soundness of the Sigma Calculus.
    • Local confluence / confluence
    • Termination
      • Reduction to Unified Expressions
      • Reduction to Distribution Termination
      • Termination of the Distribution Calculus
        • Renaming Epxressions
        • Contexts and patterns
        • Splitting
        • Reduction for Patterns
        • Preservation
      • Termination
    • Substitutivity proofs of reduction.
      • Substitutivity for the Lambda Calculus with Pairs
      • Substitutivity for Call-by-Value System F
  • Chapter 7 : Modular Syntax
    • Tools for modular syntax with binders
      • Basic definitions
    • MetaCoq Commands
    • Tactics for modular syntax
    • Reduction and Values
      • Single-step reduction
      • Multi-step reduction
      • Substitutivity
    • Typing, Context Morphism Lemmas, and Preservation
    • Variadic Preservation
      • Single-step reduction
      • Substitutivity
      • Variadic typing
      • Preservation
    • Weak Head Normalisation
    • Schäfer's Expression Relation
    • Raamsdonk's Characterisation
    • Logical Relation
    • Decidability of Beta Equivalence
      • Reduction, multireduction, and their properties
      • Algorithmic Equivalence
      • Logical Equivalence
      • Main Lemma.
      • Declarative Equivalence
  • Case Study - Preservation, Weak Head Normalisation, and Strong Normalisation for Modular Syntax
    • mini-ML: Variables
      • Preservation
      • Weak Head Normalisation
      • Strong Normalisation
    • MiniML: Boolean expressions
      • Preservation
      • Weak Head Normalisation
      • Strong Normalisation
    • mini-ML: Arithmetic terms
      • Preservation
      • Weak Head Normalisation
      • Strong Normalisation
    • mini-ML: Lambda expressions
      • Preservation
      • Weak Head Normalisation
      • Strong Normalisation
    • Composition
      • Definition of typing
      • Definition of evaluation
      • Type preservation
      • Weak Normalisation
      • Strong Normalisation
  • Chapter 10 - Type Safety for F-Sub
    • Part 1 : System F
      • Properties of Subtyping
      • Type Safety
        • Progress
        • Preservation
  • Appendix A -- Abstract Reduction Systems.
    • Tactics
    • Reflexive, Transitive closure
    • Strong Normalisation
    • Local confluence, confluence, and Newman's Lemma.
  • Appendix B: Strong Normalisation à la Girard
    • Strong Normalisation
      • SN Closure under Weakening
    • The Reducibility Candidates/Logical Predicate
    • Closure under beta expansion and the fundamental theorem
  • General Header Autosubst - Assumptions and Definitions
    • Axiomatic Assumptions
      • Functional Extensionality
    • Functor Instances
      • List Instance
      • Prod Instance
      • Function 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.
    • Notations for unscoped syntax
    • Tactics for unscoped syntax
  • Autosubst Header for Scoped 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 substitution primitives
    • Variadic Substitution Primitives
    • Notations for Scoped Syntax
    • Tactics for Scoped Syntax
    • Type classes for renamings.
Generated by coqdoc and improved with CoqdocJS