The full table of content of the development is accessible here. To complement it, here is an outline of the development’s main files, roughly in dependency order.
| File | Description |
|---|---|
| Utils | Basic generically useful definitions, notations, tactics… |
| [PERTactics] | Ltac2 tactics to manipulate partial equivalence relations. |
Primarily in the Syntax folder, contains definitions related to the syntax of terms, independent of typing: contexts, untyped reduction, normal forms, weakenings… See also the AutoSubst folder, which contains everything related to the AutoSubst tool.
Syntax.BasicAst | Definitions preceding those of the AST of terms (for now, only sorts) AutoSubst.Ast | Abstract syntax tree, definitions of renamings, substitutions and many lemmas. Generated using the AutoSubst tool. Notations | Notations for all judgments used throughout the development. It can be used as an index for notations! Syntax.NormalForms | Definition of normal and neutral forms, and properties. Syntax.UntypedReduction | Definition and basic properties of untyped reduction, used to define algorithmic typing.
Primarily in the Typing folder. We gather the important properties of typing in TypingProperties.PropertiesDefinition, then derive their consequences in a series of files. Finally, we show that these properties are consequences of the fundamental lemma of the (proper instantiations of the) logical relation in TypingProperties.LogRelConsequences. This file also contains derivations of important meta-theoretic properties such as canonicity, consistency…
| File | Description |
|---|---|
| GenericTyping | A generic notion of typing, used to define the logical relation. It is instantiated multiple times, with different variants of typing, to derive gradually stronger properties. |
| DeclarativeTyping | Specification of conversion and typing, in a standard, declarative fashion. |
| TypingProperties.DeclarativeInstance | Proof that declarative typing is an instance of generic typing. |
| TypingProperties.PropertiesDefinition | Definition of the high-level, abstract properties of conversion and typing, that we obtain as consequences of the logical relation. |
| TypingProperties.LogRelConsequences | Proofs that the properties from TypingProperties.PropertiesDefinition are consequences of the logical relation. |
The files in the LogicalRelation.Definition folder give the definition of each of the cases of the logical relation, which are assembled in LogicalRelation.Def. Files in the LogicalRelation folder derive general properties of the logical relation, and those in LogicalRelation.Introductions derive the reducibility some term formers.
However the logical relation as defined in LogicalRelation.Def is not a model of typing, only its closure under reducible substitution is. This is defined in Validity.Validity, and the remaining properties are proven in the LogRel.Validity folder.
Finally, Fundamental derives the fundamental theorem of the logical relation. Note that only TypingProperties.LogRelConsequences directly uses this fundamental lemma. All other files only use the properties in TypingProperties.PropertiesDefinition instead.
| File | Description |
|---|---|
| LogicalRelation.Def | Contains the logical relation’s definition. |
| LogicalRelation.Induction | We derive by hand better induction principles for the logical relation, which handle some repacking and universe-related shenanigans once and for all. |
| LogicalRelation.Escape | The escape lemma: the logical relation implies conversion/typing. |
| Validity.Validity | Definition of validity: closure of the logical relation under substitution. |
| Fundamental | Fundamental theorem: declarative typing implies the logical relation (for any generic instance). |
The second big part of the formalisation explores algorithmic presentations of the type system, and decision procedures.
| File | Description |
|---|---|
| AlgorithmicTyping | Definition of type-directed conversion and algorithmic typing, as inductive predicates. |
| Algorithmic.UntypedConversion | Alternative, fully term-directed conversion checking algorithm, as inductive predicate. |
| Algorithmic.Bundled | Algorithmic judgments bundled with their pre-conditions, and tailored induction principles showing invariant preservation in the “algorithm”. |
The various functions for conversion-checking and type-checking are defined and verified in the Decidability folder.
| File | Description |
|---|---|
| Decidability.Functions | Definition of the conversion and type-checker. |
| Decidability.UntypedFunctions | Implementation of untyped conversion. |
| Decidability.Decidability | Type-checking is decidable. |
| Decidability.Execution | Example executions of the type checker, in Coq. |
The Misc folder contains files that are not strictly necessary for the development, but that we keep around for curiosity.
| File | Description |
|---|---|
| Misc.Positivity | A discrepancy in positivity-checking inductive types between Agda and Coq, which was a source of difficulties when first setting up the logical relation in Coq. |