The Essence of Gradual Typing

Gradual typing enables programming languages to seamlessly combine dynamic and static checking. Language researchers and designers have extended a wide variety of type systems to support gradual typing. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs.

In this talk, Éric Tanter will give an informal introduction to gradual typing, and present some advanced applications of the approach to effect systems, refinement types and security types. He will then present a formal foundation for gradual typing, drawing on principles from abstract interpretation, called Abstracting Gradual Typing (AGT for short). Gradual languages designed with the AGT approach satisfy, by construction, the established criteria for gradually-typed languages. He reports on his experience applying AGT to various typing disciplines, highlighting the challenges of achieving type soundness (and not only type safety) when types are expected to enforce semantic properties like parametricity and noninterference.

Éric Tanter is a Full Professor in the Computer Science Department of the University of Chile, currently a Visiting Researcher in the Prosecco team at Inria Paris.
He received his PhD from both the University of Nantes and the University of Chile in 2004. His research interests cover programming languages and software engineering, ranging from the theoretical underpinnings of programming languages to the empirical study of the practice of programming. He has published many articles in, and is regularly involved in the program committees and editorial boards of, major conferences and journals in these areas. Recently, he has been mostly involved in the foundations and practice of gradual typing and verification.