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.
| 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 | Definiton 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. |
| 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. |
| 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 |
| ShapeView | Technique to avoid considering non-diagonal cases for two reducibly convertible types. |
| 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. |
| File | Description |
|---|---|
| AlgorithmicTyping | Definition of the second notion of typing: algorithmic typing (and algorithmic conversion together with it). |
| LogRelConsequences | Consequences of the logical relation on declarative typing necessary to establish properties of algorithmic typing. |
| BundledAlgorithmicTyping | Algorithmic typing bundled with its pre-conditions, and a tailored induction principle showing invariant preservation in the “algorithm”. |
| AlgorithmicConvProperties | Properties of algorithmic conversion, in order to derive the second instance of generic typing, consisting of declarative typing and algorithmic conversion. |
| AlgorithmicTypingProperties | Derive the third instance of generic typing, consisting entierly of algorithmic notions. |
| File | Description |
|---|---|
| Positivity.v and Positivity.agda | Showcase the difference between Coq and Agda’s positivity checkers. |