ECOOP 2015
Sun 5 - Fri 10 July 2015 Prague, Czech Republic
Mon 6 Jul 2015 15:00 - 15:20 at Moravia III - Contracts

Typed Racket is a statically typed dialect of Racket that allows idiomatic Racket programs to be enriched with types. It can reason about many dynamically typed programming patterns while providing sound interoperability and optimizations. We have designed and are implementing an extension to Typed Racket which adds support for logical refinement types and linear integer constraints. This summary discusses our approach to implementing this novel combination of precise specifications and optimizations while maintaining sound interoperability with dynamically typed code. A PLT Redex model of the basic calculus describing our extension can be seen at https://github.com/andmkent/stop2015-redex and our development fork where we are extending Typed Racket is available at https://github.com/andmkent/typed-racket.

Adding Practical Dependent Types to Typed Racket (STOP_2015_submission_2.pdf)112KiB