PLSE Seminar Series - Ranjit Jhala, "Refinement Types for Dynamic Languages"

Explore a seminar on Refined TypeScript (RSC), a lightweight refinement type system for verifying user-defined safety properties in TypeScript programs. Delve into the challenges of dynamic, higher-order imperative programming, including value-based overloading and the impact of assignment and mutation on refinement soundness. Learn about two-phased typing, ownership-based soundness assurance, and SSA transformation for flow- and path-sensitivity. Discover how RSC establishes value-dependent properties like array access safety and downcast security in real-world benchmarks, including Octane, D3, Transducers, and the TypeScript compiler. Gain insights from Ranjit Jhala, an accomplished computer scientist with expertise in programming languages and software engineering, as he presents this joint work with Panagiotis Vekris and Benjamin Cosman.

PLSE Seminar Series Ranjit Jhala, "Refinement Types for Dynamic Languages"