Skip to content

Latest commit

 

History

History

oopsla16

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
Makefile
Makefile
 
 
README.md
README.md
 
 
SfLib.v
SfLib.v
 
 
dot.v
dot.v
 
 
dot_exs.v
dot_exs.v
 
 
dot_soundness.v
dot_soundness.v
 
 
dot_soundness_alt.v
dot_soundness_alt.v
 
 

README.md

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.