KafKa: Gradual Typing for Objects
The enduring popularity of dynamically typed languages has motivated research on \emph{gradual type systems} to allow developers to annotate legacy dynamic code piecemeal. Type soundness for a program which contains a mixture of typed and untyped code cannot mean the traditional absence of errors. While some errors will be caught at type checking time, others can only be caught as the program executes. After a decade of research it is has become difficult to separate and distill the right gradual type systems for each situation and scenario. We introduce a framework for comparing gradual type systems, combining a common source languages with \kafka, a calculus for object-oriented gradual typing, decoupling the semantics of gradual typing from those of the language. We demonstrate the usefulness of this approach by translating idealizations of four different gradually typed semantics into the calculus and discuss the implications of their respective designs.
Fri 20 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:40 | |||
11:00 25mResearch paper | KafKa: Gradual Typing for Objects ECOOP Research Papers Benjamin Chung Northeastern University, Paley Li Northeastern University, Francesco Zappa Nardelli Inria, Jan Vitek Northeastern University DOI | ||
11:25 25mResearch paper | Dependent Types for Class-based Mutable Objects ECOOP Research Papers DOI | ||
11:50 25mResearch paper | Static typing of complex presence constraints in interfaces ECOOP Research Papers Nathalie Oostvogels Vrije Universiteit Brussel, Joeri De Koster Vrije Universiteit Brussel, Belgium, Wolfgang De Meuter Vrije Universiteit Brussel DOI | ||
12:15 25mResearch paper | Mailbox Types for Unordered Interactions ECOOP Research Papers DOI |