Paper (ECOOP 2017): [pdf]

The Coq scripts compile with the command make, using coqc --version 8.6.

• dsubsup_total.v -- termination proof for plain D<:> (Section 3)
• dsubsup_total_rec.v -- termination proof for D<:> plus recursive self types and intersection types (Section 4)

Appendix A of the paper, Strong Normalization for Dependent Object Types (DOT) (PDF), describes the correspondence between the formalism on paper and the development in Coq.