Skip to content
Branch: master
Find file History
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
..
Failed to load latest commit information.
doc fixing links for theorems Apr 29, 2019
.gitignore adjusting graph for readme Apr 27, 2019
Binding.v renaming definitions and changing notations to match paper Apr 27, 2019
CanonicalForms.v removing links to theorems from proofs Apr 29, 2019
CompilerExample.v working on documentation, restructuring some lemmas Apr 24, 2019
Definitions.v renaming definitions and changing notations to match paper Apr 27, 2019
ExampleTactics.v working on documentation, restructuring some lemmas Apr 24, 2019
GeneralToTight.v prettifying some documentation Apr 27, 2019
InvertibleTyping.v a lot of additional documentation Apr 27, 2019
ListExample.v working on documentation, restructuring some lemmas Apr 24, 2019
Lookup.v fixing lookup notations in comments Apr 29, 2019
Makefile working on documentation, removing unnecessary typing notation from s… Apr 25, 2019
Narrowing.v working on documentation, removing unnecessary typing notation from s… Apr 25, 2019
PreciseFlow.v documentation for safety Apr 26, 2019
PreciseTyping.v renaming definitions and changing notations to match paper Apr 27, 2019
README.md improving paper links Apr 29, 2019
RecordAndInertTypes.v renaming definitions and changing notations to match paper Apr 27, 2019
Reduction.v links to specific parts in paper Apr 29, 2019
Replacement.v a lot of additional documentation Apr 27, 2019
ReplacementTyping.v a lot of additional documentation Apr 27, 2019
Safety.v removing links to theorems from proofs Apr 29, 2019
Sequences.v working on documentation, restructuring some lemmas Apr 24, 2019
SingletonTypeExample.v working on documentation, restructuring some lemmas Apr 24, 2019
Subenvironments.v a lot of additional documentation Apr 27, 2019
Substitution.v renaming definitions and changing notations to match paper Apr 27, 2019
TightTyping.v working on documentation, removing unnecessary typing notation from s… Apr 25, 2019
Weakening.v working on documentation, restructuring some lemmas Apr 24, 2019

README.md

pDOT Type Safety Proof

This directory contains the Coq formalization type-safety proof of the pDOT calculus that generalizes DOT by Amin et al. (2016). with paths of arbitrary length. This allows us to express path-dependent types of the form x.a.b.A as opposed to just x.A.

Link to the pDOT paper

Compiling the Proof

System requirements:

  • make
  • an installation of Coq 8.9.0, preferably through opam
  • the TLC library which can be installed through
 opam repo add coq-released http://coq.inria.fr/opam/released
 opam install -j4 coq-tlc

To compile the proof, navigate to the cloned directory and run

 cd src/extensions/paths
 make

Paper Correspondence

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.

Correspondence of Definitions

Definition In paper File Paper notations Proof notations Name in proof
Abstract Syntax Fig. 2 Definitions.v
- variable Fig. 2 Definitions.v avar
- term member Fig. 2 Definitions.v trm_label
- type member Fig. 2 Definitions.v typ_label
- path Fig. 2 Definitions.v x.a.b.c

p.a

p.b̅
p_sel x (c::b::a::nil)

p•a

p••b
path
- term Fig. 2 Definitions.v trm
- stable term Fig. 2 Definitions.v def_rhs
- value Fig. 2 Definitions.v ν(x: T)ds
λ(x: T)t
ν(T)ds
λ(T)t
val
- definition Fig. 2 Definitions.v {a = t}
{A = T}
{a := t}
{A ⦂= T}
def
- type Fig. 2 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. 3, 4 Definitions.v
- term typing Fig. 3 Definitions.v Γ ⊢ t: T Γ ⊢ t : T ty_trm
- definition typing Fig. 3 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. 3 Definitions.v tight_bounds
- subtyping Fig. 4 Definitions.v Γ ⊢ T <: U Γ ⊢ T <: U subtyp
Operational semantics Fig. 5 Reduction.v γ|t ⟼ γ'|t'
γ|t ⟼* γ'|t'
(γ, t) ⟼ (γ', t')
(γ, t) ⟼* (γ', t')
red
Path lookup Fig. 6 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. 7 Definitions.v inert T
inert Γ
inert_typ
inert
Well-formed
environments
Sec. 5.2.1 PreciseTyping.v wf
Correspondence
between a value
and type environment
Sec. 5 Definitions.v γ: Γ γ ⫶ Γ well_typed

Correspondence of Lemmas and Theorems

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

Correspondence of Examples

Example In paper File
List example Section 6.2, Figure 8 a ListExample.v
Compiler example Section 6.3, Figure 8 b CompilerExample.v
Singleton type example Section 6.4, Figure 8 c SingletonTypeExample.v

Proof Organization

Safety Proof

The Coq proof is split up into the following modules:

Examples

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

Dependency graph

You can’t perform that action at this time.