Browsing the sources
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] |
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. |
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 |
| [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. |
Algorithmic typing and its properties
| 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. |
Miscellaneous
| File |
Description |
| [Positivity.v] and [Positivity.agda] |
Showcase the difference between Coq and Agda’s positivity checkers. |
[Utils]
[BasicAst]
[Context]
[AutoSubst/]
[AutoSubst/Extra]
[Notations]
[Automation]
[NormalForms]
[UntypedReduction]
[GenericTyping]
[DeclarativeTyping]
[Properties]
[DeclarativeInstance]
[LogicalRelation]
[Induction]
[Escape]
[Reflexivity]
[Irrelevance]
[ShapeView]
[Positivity.v]
[Weakening]
[AlgorithmicTyping]
[AlgorithmicConvProperties]
[AlgorithmicTypingProperties]
[LogRelConsequences]
[BundledAlgorithmicTyping]