1.55 KB

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 an extension to DOT that aim to bridge the gap between DOT and Scala, and to experiment with new Scala features. The extension is based on the 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.

Compiling the Proof

To compile the proof, we require coq 8.8.1 and related tooling to be run in a unix-like environment. We also require coq-tlc library. We recommend installing both using opam.

opam repo add coq-released
opam pin add coq 8.8.1
opam install coq
opam install coq-tlc

Other requirements are:

  • make

To compile the proof, clone the repository to a directory called dot-calculus and run

cd dot-calculus

make will do the following:

  • compile the safety proof
  • generate documentation.