Browsing the sources
The full table of content of the development is accessible here.
To complement it, here is a rough description of the content of every file.
Utilities and AST
| File |
Description |
| [Utils] |
Basic generically useful definitions, notations, tactics… |
| [BasicAst] |
Definitions preceding those of the AST of terms: sorts, binder annotations… |
| [AutoSubst/] |
Abstract syntax tree, renamings, substitutions and many lemmas, generated using the [autosubst-ocaml] opam package. |
| [AutoSubst/Extra] |
Extra instances, notations and tactics to better handle the boilerplate generated by AutoSubst. |
| [Notations] |
Notations used throughout the development. It can be used as an index for notations! |
| [NormalForms] |
Definition of normal and neutral forms, and properties. |
| File |
Description |
| [Context] |
Definition of contexts and operations on them. |
| [Weakening] |
Definition of a well-formed weakening, and some properties. |
| [UntypedReduction] |
Definition and basic properties of untyped reduction, used to define algorithmic typing. |
| [GenericTyping] |
A generic notion of typing, used to define the logical relation, to be instantiated three times: once with the fully declarative version, once with the mixed declarative and algorithmic one, and once with the fully algorithmic one. |
Declarative typing and its properties
| File |
Description |
| [DeclarativeTyping] |
Defines the theory’s typing rules in a declarative fashion, the current definition has a single universe as well as product types and eta-conversion for functions. |
| [DeclarativeInstance] |
Proof that declarative typing is an instance of generic typing. |
Logical relation and its properties
| File |
Description |
| [LogicalRelation] |
Contains the logical relation’s (LR) definition. |
| [Induction] |
Defines the induction principles over LR. Because of universe constraints, LR needs two induction principles, one for each type levels. |
| [Escape] |
Contains a proof of the escape lemma for LR |
| [Reflexivity] |
Reflexivity of the logical relation. |
| [Irrelevance] |
Irrelevance of the logical relation: two reducibly convertible types decode to equivalent predicates. Symmetry is a direct corollary. |