Skip to content
<awesome-gh-repos>
vic

namin/dot

formalization of the Dependent Object Types (DOT) calculus
Source code at GitHub http://lamp.epfl.ch/~amin/dot/
namin/dot.json
{
  "createdAt": "2012-01-25T00:37:26Z",
  "defaultBranch": "master",
  "description": "formalization of the Dependent Object Types (DOT) calculus",
  "fullName": "namin/dot",
  "homepage": "http://lamp.epfl.ch/~amin/dot/",
  "language": null,
  "name": "dot",
  "pushedAt": "2016-09-08T13:37:52Z",
  "stargazersCount": 161,
  "topics": [
    "coq",
    "dafny",
    "meta-theory",
    "oop",
    "plt-redex",
    "twelf"
  ],
  "updatedAt": "2025-07-22T17:44:43Z",
  "url": "https://github.com/namin/dot"
}

Dependent Object Types (DOT)

Section titled “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: