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

LogRel.PERTactics: Ltac2 tactics to manipulate partial equivalence relations.

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

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

LogRel.AutoSubst.core

LogRel.AutoSubst.unscoped

LogRel.AutoSubst.Ast: abstract syntax tree, definitions of renamings, substitutions and many lemmas, generated using AutoSubst.

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

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

LogRel.Syntax.TermNotations: notations for terms in the object language, defined in a custom entry.

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

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

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

LogRel.Syntax.Sections: some very short theory of sections, useful to define strengthening lemmas.

LogRel.Syntax.All

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.TypingProperties.DeclarativeProperties: basic properties of declarative typing, showing it is an instance of generic typing.

LogRel.TypingProperties.NormalisationDefinition: definition and basic properties of deep, typed normalisation.

LogRel.TypingProperties.PropertiesDefinition: the high-level, abstract properties of conversion and typing, that we obtain as consequences of the logical relation.

LogRel.TypingProperties.SubstConsequences: consequences of stability by substitution.

LogRel.TypingProperties.TypeInjectivityConsequences: properties around injectivity and no-confusion of type constructors and many consequences, including subject reduction.

LogRel.TypingProperties.NeutralConvProperties

LogRel.TypingProperties.NormalisationConsequences: direct consequences of normalisation.

LogRel.TypingProperties.LogRelConsequences: the properties from PropertiesDefinition are consequences of the logical relation.

LogRel.LogicalRelation.Definition.Prelude: Structures employed to define the logical relation

LogRel.LogicalRelation.Definition.Universe: Definition of the logical relation for universes

LogRel.LogicalRelation.Definition.Ne: Definition of the logical relation for neutal types and terms

LogRel.LogicalRelation.Definition.Poly: Definition of the logical relation for polynomial

LogRel.LogicalRelation.Definition.Pi: Definition of the logical relation for dependent products

LogRel.LogicalRelation.Definition.Sig: Definition of the logical relation for dependent sums

LogRel.LogicalRelation.Definition.Nat: Definition of the logical relation for nat

LogRel.LogicalRelation.Definition.Empty: Definition of the logical relation for the empty type

LogRel.LogicalRelation.Definition.Id: Definition of the logical relation for indentity types

LogRel.LogicalRelation.Definition.Def: Definition of the logical relation

LogRel.LogicalRelation.Definition.Helper: Auxilliary definitions and rebundling of structures from the logical relation

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.Irrelevance: symmetry and irrelevance of the logical relation.

LogRel.LogicalRelation.Symmetry

LogRel.LogicalRelation.Transitivity

LogRel.LogicalRelation.Weakening

LogRel.LogicalRelation.Neutral

LogRel.LogicalRelation.InstKripke: combinators to instantiate Kripke-style quantifications

LogRel.LogicalRelation.Reduction

LogRel.LogicalRelation.NormalRed

LogRel.LogicalRelation.Properties

LogRel.LogicalRelation.Introductions.Universe

LogRel.LogicalRelation.Introductions.Poly

LogRel.LogicalRelation.Introductions.Pi

LogRel.LogicalRelation.Introductions.Application

LogRel.LogicalRelation.Introductions.SimpleArr

LogRel.LogicalRelation.Introductions.Nat

LogRel.LogicalRelation.Introductions.Empty

LogRel.LogicalRelation.Introductions.Sigma

LogRel.LogicalRelation.Introductions.Id

LogRel.Validity.Validity: definition of validity: closure of the logical relation under substitution.

LogRel.Validity.Irrelevance

LogRel.Validity.Properties

LogRel.Validity.ValidityTactics

LogRel.Validity.Introductions.Universe

LogRel.Validity.Introductions.Var

LogRel.Validity.Introductions.Poly

LogRel.Validity.Introductions.Pi

LogRel.Validity.Introductions.Application

LogRel.Validity.Introductions.Lambda

LogRel.Validity.Introductions.SimpleArr

LogRel.Validity.Introductions.Nat

LogRel.Validity.Introductions.Empty

LogRel.Validity.Introductions.Sigma

LogRel.Validity.Introductions.Id

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

LogRel.AlgorithmicJudgments: definition of conversion (typed and untyped

LogRel.Algorithmic.Bundled: algorithmic judgments bundled with their pre-conditions, and tailored induction principles.

LogRel.Algorithmic.TypedConvProperties

LogRel.Algorithmic.TypedConvPER

LogRel.Algorithmic.TypedConvInstances

LogRel.Algorithmic.UntypedConvSoundness: untyped conversion implies declarative typing.

LogRel.Algorithmic.UntypedTypedConv: implications between typed and untyped conversion.

LogRel.Algorithmic.AlgorithmicTypingProperties

LogRel.Algorithmic.Strengthening: proof of the strengthening property for algorithmic conversions.

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

LogRel.Checkers.Views: properties of the view-building functions.

LogRel.Checkers.CtxAccessCorrectness: correctness of the context accessing function.

LogRel.Checkers.ReductionCorrectness: properties of the reduction function.

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

LogRel.Checkers.NegativeSoundness: implementation failure implies negation of typing.

LogRel.Checkers.UntypedNegativeSoundness: implementation failure implies negation of untyped conversion.

LogRel.Checkers.Completeness: the inductive predicates imply their implementations answer positively.

LogRel.Checkers.UntypedCompleteness: the inductive predicate implies the implementation answer positively.

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

LogRel.Checkers.UntypedTermination: the implementation always terminates on well-typed inputs.

LogRel.Execution

LogRel.Decidability