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).
Compiling the Proof
To compile the proof, we require
coq 8.7.2 and related tooling to be run in a unix-like environment. We also require
coq-tlc library. We recommend installing both using
opam repo add coq-released https://coq.inria.fr/opam/released opam pin add coq 8.7.2 opam install coq opam install coq-tlc
Other requirements are:
To compile the proof, clone the repository to a directory called
dot-calculus and run
cd dot-calculus make
make will do the following:
- compile the safety proof
- generate documentation.