Permalink
Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
23 lines (19 sloc) 1.65 KB

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: