A Simple Soundness Proof for
Dependent Object Types
Our paper presents a simplified type-safety proof for the version of DOT presented at Wadlerfest 2016. This repository contains a formalization of the simple proof in Coq. The definitions of the abstract syntax and several lemmas are based on the original Coq proof that comes with Wadlerfest DOT paper.
This directory contains a Coq formalization of the DOT calculus and DOT's type safety proof. Our technique is based on eliminating bad bounds by using inert types and applying the proof recipe, as described in the OOPSLA'17 paper.
Documentation
The documentation can be accessed from the table of contents. This page
lists links to pretty printed Coq source files, but the
raw .v
files can be found in the
proof directory. In the
pretty-printed versions, the proof scripts are hidden by default, you may
click on "Show Proofs" at the top of the page to display all the
proofs, or click under the Lemma or Theorem statements to display their
proofs.
Description of the Proof
This directory contains a Coq formalization of the DOT calculus and DOT's type safety proof using the method presented in the paper. The final Progress and Preservation proofs can be found in Safety.v.
Proof Structure
The Coq proof is split up into the following modules:- Definitions.v: The main inductive definitions and functions that are used in the proof. Defines the abstract syntax and type system.
- Binding.v: Proves helper lemmas related to opening, closing, and local closure.
- Subenvironments.v: Defines and proves lemmas related to subenvironments.
- Weakening.v: Proves the Weakening Lemma.
- RecordAndInertTypes.v: Defines and proves lemmas related to record and inert types.
- Narrowing.v: Proves the Narrowing Lemma.
- OperationalSemantics.v: Defines normal forms and the operational semantics of DOT, as well as related helper lemmas.
- PreciseTyping.v: Defines and proves lemmas related to precise typing. In particular, reasons about the possible precise types that a variable can have in an inert environment.
- TightTyping.v: Defines tight typing and subtyping.
- Substitution.v: Proves the Substitution Lemma.
- InvertibleTyping.v: Defines invertible typing and proves that in an inert context, tight typing implies invertible typing (both for variables and values).
- GeneralToTight.v: Proves that in an inert context, general typing implies tight typing.
- CanonicalForms.v: Proves the Canonical Forms Lemmas for functions and objects.
- Safety.v: Proves the Progress and Preservation Theorems.
The following figure shows a dependency graph between the Coq modules.
Paper Correspondence
Below, we present a table that shows how the definitions and lemmas in the paper correspond to the Coq proof.
Paper |
Coq Proof |
||||
---|---|---|---|---|---|
Item | Description | Subitems | File | Name | Notation |
Figure 1 |
DOT abstract syntax |
variable | Definitions.v | avar | |
term member |
trm_label | ||||
type member |
typ_label | ||||
term | trm | ||||
value | val | ||||
definition | def | ||||
type | typ | ||||
Figure 2 |
DOT Type Rules |
term typing |
Definitions.v | ty_trm | G ⊢ t : T |
single-definition typing | ty_def | G ⊢ d : D | |||
multiple-definition typing | ty_defs | G ⊢ ds :: T | |||
subtyping |
subtyp | G ⊢ T <: U | |||
Figure 3 |
Tight typing rules |
term typing |
TightTyping.v | ty_trm_t | G ⊢# t : T |
subtyping |
subtyp_t | G ⊢# T <: U | |||
Definition 3.1 |
Inert context |
RecordAndInertTypes.v | inert | ||
Definition 3.2 |
Inert type |
RecordAndInertTypes.v | inert_typ | ||
Figure 4 |
Precise typing rules |
PreciseTyping.v | ty_trm_p | G ⊢! t : T | |
Theorem 3.3 |
General-to-tight typing (⊢ to ⊢#) | GeneralToTight.v | general_to_tight | ||
Lemma 3.4 |
Sel-<: replacement | GeneralToTight.v |
sel_replacement | ||
Lemma 3.5 |
Sel-<:# premise |
GeneralToTight.v | sel_premise | ||
Figure 5 |
Invertible typing rules |
for variables |
InvertibleTyping.v | ty_var_inv | G ⊢## x : T |
for values |
ty_val_inv | G ⊢##v v : T | |||
Theorem 3.6 |
Tight-to-invertible typing (⊢# to ⊢##) | for variables |
InvertibleTyping.v | tight_to_invertible | |
for values |
tight_to_invertible_v | ||||
Lemma 3.7 |
∀ to Γ(x) | CanonicalForms.v | var_typ_all_to_binds | ||
Lemma 3.8 |
∀ to λ | CanonicalForms.v | val_typ_all_to_lambda | ||
Lemma 3.9 |
μ to Γ(x) | CanonicalForms.v | var_typ_rcd_to_binds | ||
Lemma 3.10 |
μ to ν | CanonicalForms.v | val_mu_to_new | ||
Lemma 3.11 |
Narrowing | Narrowing.v | narrow_rules |
||
Figure 7 |
Operational semantics |
OperationalSemantics.v | red | e[t1 ↦ t2] | |
Definition 3.12 |
Well-typed evaluation contexts with respect to a typing context | Definitions.v | well_typed | ||
Lemma 3.15 |
Value typing |
Safety.v | val_typing | ||
Definition 3.16 |
Normal form | OperationalSemantics.v | normal_form | ||
Theorem 3.17 |
Progress | Safety.v | progress | ||
Theorem 3.18 |
Preservation | Safety.v | preservation | ||
Lemma 3.19 |
Substitution | Substitution.v | subst_ty_trm |
Compiling the Proof
To compile the proof, we require coq 8.6
and related tooling
to be run in a unix-like environment. In particular, we require
the following tools (all version 8.6) in the PATH
enviroment variable:
coqc
coqtop
coqdep
coqdoc
coqmakefile
make
sed
graphviz
(optional, requried for file/lemma dependency graph)coq-dpdgraph
(optional, requried for lemma dependency graph)grep
(optional, requried for lemma dependency graph)paste
(optional, requried for lemma dependency graph)xargs
(optional, requried for lemma dependency graph)
To compile the proof, run
This will do the following:git clone https://github.com/amaurremi/dot-calculus
cd dot-calculus/src/simple-proof
make
- compile the
tlc
library; - compile the safety proof;
- generate documentation.