Refinement types for TypeScript (and Typed Racket) [OT]

This is about language design.

From a post in the Lambda the Ultimate Blog ( PLDI 2016 Proceedings now available on-line, free for 3 weeks | Lambda the Ultimate ) I've found two papers about the experimental implementation of refinement types in Typed Racket and TypeScript (that are a statically typed Scheme and Java Script):

"available on-line, free to all until 2 weeks after the conference", from this page:

"Refinement types for TypeScript", by Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala (PDF file):

Try it online:

"Occurrence typing modulo theories" by Andrew M. Kent, David Kempe, Sam Tobin-Hochstadt (PDF file):

The article about TypeScript is the most interesting of the two. Rust cares a lot about code correctness, and it's already very-strongly and very-statically typed, so to me it seems a good language to introduce refinement types, despite their current limits.