The list of lemmas and theorems of the paper is replicated in Assumptions.
General tactics, lemmas and notations are defined in Util.
We define the syntax for two languages: the Calculus of Constructions (CC) and our own Ghost Type Theory (GTT). BasicAST contains the notion of mode and of universe levels. autosubst/CCAST.sig and autosubst/GAST.sig are used to generate the autosubst/CCAST and autosubst/GAST modules. autosubst/core, autosubst/unscoped and SubstNotations contain the Autosubst library and some notations. autosubst/RAsimpl contains implementation for the rasimpl tactic, whereas [autosubst/CCAST_rasimpl] and [autosubst/GAST_rasimpl] provide the corresponding instances for CC and GTT.
ContextDecl defines contexts for both theories.
| Module | Description |
|---|---|
| CastRemoval | Operation which removes casts from a term. |
| Scoping | Definition of scoping (checks modes) |
| TermMode | Syntactic computation of mode |
| Univ | Utility on universes (successor, max…) |
| TermNotations | Some shorthands for implication and so on… |
| Typing | Conversion and typing judgements |
| BasicMetaTheory | Meta-theory like substitution and validity |
| Module | Description |
|---|---|
| CScoping | Scoping |
| CTyping | Typing |
| CCMetaTheory | Substitution and the like |
| Module | Description |
|---|---|
| Erasure | Erasure translation |
| Revival | Revival translation |
| Param | Parametricity translation |
| Model | Consequences of the model |
| Admissible | Simpler typing rules for GTT, assuming injectivity of Π-types |
| FreeTheorem | Proof-of-concept free theorem for GTT |
| Examples | Examples from the paper |
| Module | Description |
|---|---|
| RTyping | Typing for GRTT |
| Potential | Notion of potential translation |
| ElimReflection | Translation from GRTT to GTT |
We handle booleans directly in the syntax of GTT and CC, but for natural numbers and vectors we opted for a different approach: we build the terms directly in Coq as it is much easier to do. We then assume constants in CC with exactly the types we inhabit in TransNat and TransVec.
| Module | Description |
|---|---|
| TransNat | Erasure and parametricity for nat |
| TransVec | Erasure and parametricity for vec |