A good proof is one that makes us wiser. -- Yuri Manin

Formalizations of the Dependent Object Types (DOT) calculus, from the bottom up, with soundness proofs at each step.

• Towards Strong Normalization for Dependent Object Types (ECOOP'17) [pdf]

  • D<:> with extensions

• From F to DOT: Type Soundness Proofs with Definitional Interpreters (POPL'17) [pdf]

  • STLC
  • F<:
  • F<: Equivalence with Small-Step
  • F<: with Mutable References
  • F<: with Exceptions
  • F<:> from the System D Square
  • D<:> from the System D Square
  • DOT in Big-Step
  • older developments from 2015

• Type Soundness for Dependent Object Types (OOPSLA'16) [pdf]

  • DOT in small-step

• Foundations of Path-Dependent Types (OOPSLA'14) [pdf]

  • muDOT