Adding Practical Dependent Types to Typed Racket
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|
Mon 6 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:40 - 15:40
|Adding Practical Dependent Types to Typed Racket|