Skip to content

Latest commit

 

History

History
24 lines (16 loc) · 726 Bytes

README.md

File metadata and controls

24 lines (16 loc) · 726 Bytes

Dependent Object Types (DOT)

The DOT calculus proposes a new foundation for Scala's type system.

DOT has been presented at the FOOL 2012 workshop (PDF).

We now have several mechanized type safety proofs. This repo implements the wadlerfest model in Coq, based on previous work in the namin/dot and TiarkRompf/minidot repos.

Installation

Works in Coq 8.4.6 and OCaml 4.02.3.

  • opam switch create with-wadlerfest-dot 4.02.3
  • eval $(opam env)
  • opam pin add coq 8.4.6

Then, run make from the ln directory.