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

To compile the proof, run

git clone https://github.com/amaurremi/dot-calculus cd dot-calculus/src/simple-proof
make

This will do the following:

• compile the tlc library;
• compile the safety proof;
• generate documentation.