ECOOP 2015
Sun 5 - Fri 10 July 2015 Prague, Czech Republic
Wed 8 Jul 2015 11:30 - 12:00 at Bohemia - Gradual Typing Chair(s): John Boyland

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. 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. First, we empirically demonstrate the ubiquity of value-based overloading. Next, we distill it into a core source language with union and intersection types. We formalize the trust phase as an elaboration to a simply typed target language without overloading, but with DEAD-casts and formalize the second phase that discharges the casts via classical refinement typing. Finally, we prove the equivalence of source and target to establish the end-to-end soundness of two-phase typing, thereby providing a new foundation for building static analyses for dynamic languages.

Wed 8 Jul
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:00: Gradual TypingResearch Track at Bohemia
Chair(s): John BoylandUniversity of Wisconsin, Milwaukee
10:30 - 11:00
Towards Practical Gradual Typing
Research Track
Asumu TakikawaNortheastern University, Daniel FelteyNortheastern University, Earl DeanIndiana University, Robby FindlerNorthwestern University, Matthew FlattUniversity of Utah, Sam Tobin-HochstadtIndiana University, Matthias FelleisenNortheastern University
11:00 - 11:30
TreatJS: Higher-Order Contracts for JavaScripts
Research Track
Matthias KeilUniversity of Freiburg, Peter ThiemannUniversity of Freiburg
Media Attached
11:30 - 12:00
Trust, but Verify: Two-Phase Typing for Dynamic Languages
Research Track
Panagiotis VekrisUniversity of California, San Diego, Benjamin CosmanUniversity of California, San Diego, Ranjit JhalaUniversity of California, San Diego