A Path to Full Dependent Types in DOT
November 26, 2019
I recently joined forces with Tiark Rompf to lay the groundwork for future versions of the Scala programming language. We are investigating extensions of the DOT calculus in order to bring full dependent types into the system.
The current proof efforts in Coq can be found in the main DOT repository on github.