Abstract

We are in the process of extending Typed Racket with a practical set of dependent types. This addition will allow more programs to typecheck, eliminate more runtime errors, and allow additional optimizations to be soundly performed. In this informal example-driven talk I will report on the progress of this extension and demonstrate how it enables more dynamically typed programs to gradually adopt a more statically verified specification.

For spoilers and a more detailed abstract describing this work, you may also peruse our recent STOP 2015 submission: https://github.com/andmkent/stop2015/blob/master/dtr-stop2015.pdf