Project Page
Index
Table of Contents
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.