Extensions for Dependent Object Types

We are working on type-safe extensions to the Dependent Object Types (DOT) calculus as defined by Amin et al. in their Wadlerfest paper.

We developed a simplified, modular version of the original DOT soundness proof. For details, see our technical report.

Our extensions are based on that simplified proof.

Our DOT extensions are:

• mutation (adding mutable references to DOT) (proof | technical report)
• expanded type paths (adding type selections on full paths of the form p.A instead of x.A, where p is a path and x is a variable) (proof in progress)
• initialization order (developing a sound initialization order) (proof in progress)