- 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
- big-step