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

LogRel.PERTactics

LogRel.Syntax.BasicAst

LogRel.AutoSubst.core

LogRel.AutoSubst.unscoped

LogRel.AutoSubst.Ast

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

LogRel.Syntax.Context

LogRel.Syntax.Notations

LogRel.Syntax.TermNotations

LogRel.Syntax.NormalForms

LogRel.Syntax.Weakening

LogRel.Syntax.UntypedReduction

LogRel.Syntax.Sections

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.Normalisation

LogRel.TypingProperties.PropertiesDefinition

LogRel.TypingProperties.DeclarativeProperties

LogRel.TypingProperties.SubstConsequences

LogRel.TypingProperties.TypeConstructorsInj

LogRel.TypingProperties.NeutralConvProperties

LogRel.TypingProperties.NormalisationConsequences

LogRel.TypingProperties.LogRelConsequences

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

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.AlgorithmicTyping: definition of algorithmic conversion and typing.

LogRel.Algorithmic.UntypedAlgorithmicConversion

LogRel.Algorithmic.BundledAlgorithmicTyping

LogRel.Algorithmic.AlgorithmicConvProperties

LogRel.Algorithmic.AlgorithmicTypingProperties

LogRel.Algorithmic.Strengthening

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

LogRel.Decidability.UntypedFunctions

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

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

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

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

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

LogRel.Decidability.UntypedSoundness

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

LogRel.Decidability.UntypedNegativeSoundness: implementation failure implies negation of typing for untyped conversion.

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

LogRel.Decidability: type-checking is decidable.

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