formalization of the Dependent Object Types (DOT) calculus
Switch branches/tags
Nothing to show
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.

Dependent Object Types (DOT)

The DOT calculus proposes a new type-theoretic foundation for languages like Scala. The latest rules (PDF) are for a small-step storeless variant with full subtyping lattice, recursive types including their subtyping, and dependent method types. Here is the corresponding mechanized soundness proof.

From F to DOT in Small-Step:

Historical development: