Skip to content
<open-source>
Oeiuwq Faith Blog OpenSource Porfolio

themaplelab/dot-public

Collection of some type safety proofs of the DOT calculus
Source code at GitHub null
themaplelab/dot-public.json
{
  "createdAt": "2020-05-29T15:27:05Z",
  "defaultBranch": "master",
  "description": "Collection of some type safety proofs of the DOT calculus",
  "fullName": "themaplelab/dot-public",
  "homepage": null,
  "language": "HTML",
  "name": "dot-public",
  "pushedAt": "2020-10-18T07:25:46Z",
  "stargazersCount": 1,
  "topics": [],
  "updatedAt": "2021-11-21T15:00:01Z",
  "url": "https://github.com/themaplelab/dot-public"
}

The DOT (Dependent Object Types) Calculus

Section titled “The DOT (Dependent Object Types) Calculus”

The DOT Calculus is a formalization of the Scala programming language focusing on path-dependent types.

This repo collects a bunch of type safety proofs of the DOT calculus.

Simpler Type Safety for DOT Calculi

Section titled “Simpler Type Safety for DOT Calculi”

Some simplifications of the Rapoport et al. type safety proof are provided in dot-simpler folder.

Sound Object Initialization in DOT

Section titled “Sound Object Initialization in DOT”

The ιDOT calculus is a DOT Calculus which enforces a sound object initialization order using a type and effect system. The calculus and several of its extensions are provided in the idot folder.