LogRel.Utils: basic generically useful definitions, notations, tactics…

LogRel.BasicAst: definitions preceding those of the AST of terms: sorts, binder annotations…

LogRel.AutoSubst.core

LogRel.AutoSubst.unscoped

LogRel.AutoSubst.Ast

LogRel.AutoSubst.Extra: extra content to better handle the boilerplate generated by AutoSubst.

LogRel.Context: definition of contexts and operations on them.

LogRel.Notations: notations for conversion, typing and the logical relations.

LogRel.NormalForms: definition of normal and neutral forms, and properties.

LogRel.Weakening: definition of well-formed weakenings, and some properties.

LogRel.UntypedReduction: untyped reduction, used to define algorithmic typing.

LogRel.UntypedValues

LogRel.GenericTyping: the generic interface of typing used to build the logical relation.

LogRel.DeclarativeTyping: specification of conversion and typing, in a declarative fashion.

LogRel.DeclarativeInstance: proof that declarative typing is an instance of generic typing.

LogRel.LogicalRelation: Definition of the logical relation

LogRel.LogicalRelation.Induction: good induction principles for the logical relation.

LogRel.LogicalRelation.Escape: the logical relation implies conversion/typing.

LogRel.LogicalRelation.ShapeView: relating reducibility witnesses of reducibly convertible types.

LogRel.LogicalRelation.Reflexivity: reflexivity of the logical relation.

LogRel.LogicalRelation.Irrelevance: symmetry and irrelevance of the logical relation.

LogRel.LogicalRelation.Weakening

LogRel.LogicalRelation.Universe

LogRel.LogicalRelation.Neutral

LogRel.LogicalRelation.Transitivity

LogRel.LogicalRelation.Reduction

LogRel.LogicalRelation.NormalRed

LogRel.LogicalRelation.Application

LogRel.LogicalRelation.SimpleArr

LogRel.LogicalRelation.Id

LogRel.Validity

LogRel.Substitution.Irrelevance

LogRel.Substitution.Properties

LogRel.Substitution.Escape

LogRel.Substitution.Conversion

LogRel.Substitution.Reflexivity

LogRel.Substitution.Reduction

LogRel.Substitution.SingleSubst

LogRel.Substitution.Introductions.Application

LogRel.Substitution.Introductions.Universe

LogRel.Substitution.Introductions.Poly

LogRel.Substitution.Introductions.Pi

LogRel.Substitution.Introductions.Lambda

LogRel.Substitution.Introductions.SimpleArr

LogRel.Substitution.Introductions.Var

LogRel.Substitution.Introductions.Nat

LogRel.Substitution.Introductions.Empty

LogRel.Substitution.Introductions.Sigma

LogRel.Substitution.Introductions.Id

LogRel.Fundamental: declarative typing implies the logical relation for any generic instance.

LogRel.AlgorithmicTyping: definition of algorithmic conversion and typing.

LogRel.DeclarativeSubst: stability of declarative typing by substitution.

LogRel.TypeConstructorsInj: injectivity and no-confusion of type constructors, and many consequences, including subject reduction.

LogRel.Normalisation: well-typed terms always reduce to a normal form.

LogRel.Consequences: important meta-theoretic consequences of normalization: canonicity of natural numbers and consistency.

LogRel.BundledAlgorithmicTyping: algorithmic typing bundled with its pre-conditions, and a tailored induction principle.

LogRel.AlgorithmicConvProperties: properties of algorithmic conversion.

LogRel.AlgorithmicTypingProperties: properties of algorithmic typing.

LogRel.TypeUniqueness: all types for a term are convertible.

LogRel.Decidability.Functions: conversion and type-checker implementation.

LogRel.Decidability.Soundness: the implementations imply the inductive predicates.

LogRel.Decidability.Completeness: the inductive predicates imply the implementation answer positively.

LogRel.Decidability.Termination: the implementation always terminates on well-typed inputs.

LogRel.Decidability: type-checking is decidable.

LogRel.TermNotations

LogRel.Decidability.Execution: example executions of the type checker, in Coq.

LogRel.Positivity