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.


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:

The following figure shows a dependency graph between the Coq modules.

Please run 'make graph' in the proof directory to generate this graph.

Paper Correspondence

Below, we present a table that shows how the definitions and lemmas in the paper correspond to the Coq proof.

Coq Proof
Item Description Subitems File Name Notation
Figure 1
DOT abstract syntax
variable Definitions.v avar
term member
type member
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
subtyp G ⊢ T <: U
Figure 3
Tight typing rules
term typing
TightTyping.v ty_trm_t G ⊢# t : T
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
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
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
Other requirements are:
  • 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

git clone https://github.com/amaurremi/dot-calculus cd dot-calculus/src/simple-proof
This will do the following: