Skip to content

amaurremi/dot-calculus

master
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
src
 
 
 
 
 
 

Extensions for Dependent Object Types

The DOT (Dependent Object Types) calculus by Amin et al. (2016) aims to formalizes Scala, specifically, abstract type members and path-dependent types.

This repository contains type-safe extensions to DOT that aim to bridge the gap between DOT and Scala, and to experiment with new Scala features. The extensions are based on our simple type-safety proof, which we started as a fork of the original proof as presented by Amin et al. (2016).

If you want to understand the DOT safety proof, or are interested in creating your own extensions to DOT, you can read our OOPSLA paper, and check out the corresponding Coq proof.

This repo contains:

  • the simple DOT safety proof
  • extensions of DOT with:
    • paths of arbitrary length (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 | paper)
    • mutation (adding mutable references to DOT) (proof | technical report)
    • initialization order (developing a sound initialization order) (proof in progress)

About

Adding extensions to DOT calculus

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages