This repository contains the Coq formalization typesafety proof of
the pDOT calculus
that generalizes DOT by Amin et al. (2016).
with paths of arbitrary length. This allows
us to express pathdependent types of the form x.a.b.A
as opposed to
just x.A
.
System requirements:
opam repo add coqreleased http://coq.inria.fr/opam/released
opam install j4 coqtlc
To compile the proof, run
git clone https://github.com/amaurremi/dotcalculus.git
cd src/extensions/paths
make
This repository formalizes the typesafety proof of the pDOT calculus as presented in our paper. Specifically, it defines the calculus itself (its abstract syntax (paper, Coq), type system (paper, Coq), and operational semantics (paper, Coq)). The Type Soundness Theorem (paper, Coq) proves that welltyped terms in pDOT either diverge (i.e. run forever) or reduce to a normal form, which includes values (functions and objects) or paths. Since the operational semantics does not reduce paths we present an Extended Type Soundness Theorem (paper, Coq) defined in terms of the above reduction relation extended with the lookup operation (paper, Coq) that looks up paths in the runtime environment. This theorem states that a welltyped term either diverges or reduces to a value (which does not include paths).
The pDOT calculus is formalized using the locally nameless representation with cofinite quantification in which free variables are represented as named variables, and bound variables are represented as de Bruijn indices.
We include the Sequences library by Xavier Leroy into our development to reason about the reflexive, transitive closure of binary relations.
Definition  In paper  File  Paper notations  Proof notations  Name in proof 

Abstract Syntax  Fig. 1  Definitions.v  
 variable  Fig. 1  Definitions.v  avar 

 term member  Fig. 1  Definitions.v  trm_label 

 type member  Fig. 1  Definitions.v  typ_label 

 path  Fig. 1  Definitions.v  x.a.b.c p.a p.b̅ 
p_sel x (c::b::a::nil) p•a p••b 
path 
 term  Fig. 1  Definitions.v  trm 

 stable term  Fig. 1  Definitions.v  def_rhs 

 value  Fig. 1  Definitions.v  ν(x: T)ds λ(x: T)t 
ν(T)ds λ(T)t 
val 
 definition  Fig. 1  Definitions.v  {a = t} {A = T} 
{a := t} {A ⦂= T} 
def 
 type  Fig. 1  Definitions.v  {a: T} {A: T..U} ∀(x: T)U p.A p.type μ(x: T) T ∧ U ⊤ ⊥ 
{a ⦂ T} {A >: T <: U} ∀(T)U p↓A {{p}} μ(T) T ∧ U ⊤ ⊥ 
typ 
Type System  Fig. 2  Definitions.v  
 term typing  Fig. 2  Definitions.v  Γ ⊢ t: T  Γ ⊢ t : T 
ty_trm 
 replacement operation<a href=#simplifiedreplacementdefinition>*</a>  Fig. 9  Definitions.v  T[q/p]=U (replacing path p with q in T yields U)  repl_typ p q T U 
ty_trm 
 definition typing  Fig. 2  Definitions.v  p; Γ ⊢ d: T  x; bs; Γ ⊢ d : T (single definition) x; bs; Γ ⊢ d :: T (multiple definitions) Here, p= x.bs , i.e. x is p’s receiver, and bs are p’s fields in reverse order 
ty_def ty_defs 
 tight bounds  Fig. 2  Definitions.v  tight_bounds 

 subtyping  Fig. 2  Definitions.v  Γ ⊢ T <: U  Γ ⊢ T <: U 
subtyp 
Operational semantics  Fig. 3  Reduction.v  γt ⟼ γ’t’ γt ⟼* γ’t’ 
(γ, t) ⟼ (γ', t') (γ, t) ⟼* (γ', t') 
red 
Path lookup  Fig. 4  Lookup.v  γ ⊢ p ⤳ s γ ⊢ s ⤳* s’ 
γ ⟦ p ⤳ s ⟧ γ ⟦ s ⤳* s' ⟧ 
lookup_step 
Extended reduction  Sec. 5  Safety.v  γt ↠ γ’t’ γt ↠* γ’t’ 
(γ, t) ↠ (γ', t') (γ, t) ↠* (γ', t') 
extended_red 
Inert and record types  Fig. 5  Definitions.v  inert T inert Γ 
inert_typ inert 

Wellformed environments 
Sec. 5.2.1  PreciseTyping.v  wf 

Correspondence between a value and type environment 
Sec. 5  Definitions.v  γ: Γ  γ ⫶ Γ 
well_typed 
The presented definition of replacement excludes the index n
which, in the submitted version of the paper, indicated precisely which occurrence of a path p
in a type T
should be replaced with q
.
More specifically, in the submitted version of the paper, the replacement operation was defined as T[q/p,n]
which states that
T
has at least n
paths,n
th path in T
starts with p
, andp
is replaced with q
, yielding the type T[q/p,n]
.We simplified the definition of replacement by generalizing it so that it is not tied to a specific index n
.
The new definition of replacement is T[q/p]
which indicates that some occurrence of p
in T
is replaced with q
.
The final version of the paper, which we include in the artifact, presents this simplified replacement operation.
Theorem  File  Name in proof 

Theorem 5.1 (Soundness)  Safety.v  safety 
Theorem 5.2 (Extended Soundness)  Safety.v  extended_safety 
Lemma 5.3 (Progress)  Safety.v  progress 
Lemma 5.4 (Preservation)  Safety.v  preservation 
Lemma 5.5  CanonicalForms.v  canonical_forms_fun 
Example  In paper  File 

List example  Figure 6 a  ListExample.v 
Compiler example  Figure 6 b  CompilerExample.v 
Singleton type example  Figure 6 c  SingletonTypeExample.v 
The Coq proof is split up into the following modules:
The following figure shows a dependency graph between the Coq modules: