Trust, but Verify: Two-Phase Typing for Dynamic Languages

By Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala. 2015

8 citations recorded by the source corpus.

A key challenge when statically typing so-called dynamic languages is the ubiquity of value-based overloading, where a given function can dynamically reflect upon and behave according to the types of its arguments. Thus, to establish basic types, the analysis must reason precisely about values, but in the presence of higher-order functions and polymorphism, this reasoning itself can require basic types. In this paper we address this chicken-and-egg problem by introducing the framework of two-phased typing. The first “trust” phase performs classical, i.e. flow-, path- and value-insensitive type checking to assign basic types to various program expressions. When the check inevitably runs into “errors” due to value-insensitivity, it wraps problematic expressions with DEAD-casts, which explicate the trust obligations that must be discharged by the second phase. The second phase uses refinement typing, a flow- and path-sensitive analysis, that decorates the first phase’s types with logical predicates to track value relationships and thereby verify the casts and establish other correctness properties for dynamically typed languages.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Program Analysis & Verification, Software Engineering

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Program Analysis & Verification

In Software Engineering

Citations in the corpus

Do Machine Learning Models Produce TypeScript Types that Type Check? (2023, methodology): “Although this paper focuses on type migration for TypeScript, there are several other gradual type systems for JavaScript [15, 22, 30, 49].”
Refinement types for TypeScript (2016, methodology): “Second, RSC accounts for dynamic typing by using a recently proposed technique called two-phase typing [36], where dynamic behaviors are specified via union and intersection types, and verified by reduction to refinement typing.”