Tue 25 Jun 2019 08:50 - 09:10 at 224AB - Type Systems I Chair(s): Ranjit Jhala

Gradual typing combines static and dynamic typing in the same program. Siek et al. (2015) describe five criteria for gradually typed languages, including type soundness and the gradual guarantee. A significant number of languages have been developed in academia and industry that support some of these criteria (TypeScript, Typed Racket, Safe TypeScript, Transient Reticulated Python, Thorn, etc.) but relatively few support all the criteria (Nom, Gradualtalk, Guarded Reticulated Python). Of those that do, only Nom does so efficiently. The Nom experiment shows that one can achieve efficient gradual typing in languages with only nominal types, but many languages have structural types: function types, tuples, record and object types, generics, etc.

In this paper we present a compiler, named Grift, that addresses the difficult challenge of efficient gradual typing for structural types. The input language includes a selection of difficult features: first-class functions, mutable arrays, and recursive types. We show that a close-to-the-metal implementation of run-time casts inspired by Henglein's coercions eliminates all of the catastrophic slowdowns without introducing significant average-case overhead. As a result, Grift exhibits lower overheads than those of Typed Racket.

Tue 25 Jun

Displayed time zone: Tijuana, Baja California change

08:30 - 09:30
Type Systems IPLDI Research Papers at 224AB
Chair(s): Ranjit Jhala University of California, San Diego
08:30
20m
Talk
Verifying Message-Passing Programs with Dependent Behavioural Types
PLDI Research Papers
Alceste Scalas Aston University, Birmingham, UK, Nobuko Yoshida Imperial College London, Elias Benussi Faculty Science Ltd
Pre-print
08:50
20m
Talk
Toward Efficient Gradual Typing for Structural Types via Coercions
PLDI Research Papers
Andre Kuhlenschmidt Indiana University, Deyaaeldeen Almahallawi Indiana University, Jeremy G. Siek Indiana University, USA
09:10
20m
Talk
Bidirectional Type Checking for Relational Properties
PLDI Research Papers
Ezgi Çiçek Facebook London, Weihao Qu University at Buffalo, SUNY, Gilles Barthe IMDEA Software Institute, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems
Media Attached