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.

• From F to DOT: Type Soundness Proofs with Definitional Interpreters [pdf]

  • big-step
    • simply typed lambda calculus
    • F_<:
    • D_<: (F_<: with first-class types and lower bounds)
    • D_<: with state (add mutable references to D_<:)
    • full DOT (D_<: plus intersection and union types, recursive self types, compound objects, ...)
  • back to small-step
    • sketch
    • full DOT

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

  • muDOT