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


#1

This is about language design.

From a post in the Lambda the Ultimate Blog ( http://lambda-the-ultimate.org/node/5350 ) 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:
http://dl.acm.org/citation.cfm?id=2908080&preflayout=flat

“Refinement types for TypeScript”, by Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala (PDF file):
http://dl.acm.org/ft_gateway.cfm?id=2908110&ftid=1734104&dwn=1&CFID=795220742&CFTOKEN=70861257

Code:


Try it online:
http://goto.ucsd.edu/~pvekris/refscript

“Occurrence typing modulo theories” by Andrew M. Kent, David Kempe, Sam Tobin-Hochstadt (PDF file):
http://dl.acm.org/ft_gateway.cfm?id=2908091&ftid=1734093&dwn=1&CFID=795220742&CFTOKEN=70861257

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