Latest commit ef1143d Oct 10, 2016

Type Soundness for Dependent Object Types (DOT)

Mechanization in Coq

The Coq scripts compile with the command make, using coqc --version 8.4pl6 (July 2015).

  • dot.v -- model and common infrastructure and lemmas
  • dot_soundness.v -- main soundness proof, based on subtyping transitivity pushback
  • dot_soundness_alt.v -- alternative soundness proof, based on directly invertible value typing aka possible types
  • dot_exs.v -- some examples, just sanity checks for expressivity

Appendix A of the paper, Type Soundness for Dependent Object Types (DOT) (PDF), outlines a correspondence between the formalism on paper and in Coq.