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


This is about language design.

From a post in the Lambda the Ultimate Blog ( ) 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.

Blog post: A Formal Verification of Rust's Binary Search Implementation
Correctness, integral overflows