The Essence of Gradual Typing

​Professor Éric Tanter, University of Chile

Abstract: 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. 

Based on an understanding of gradual types as abstractions of static types, we have developed systematic foundations for gradual typing based on 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. After a brief introduction to AGT, this talk reports on our experience applying AGT to various typing disciplines, in particular information-flow security typing.

Category Seminar
Location: ES51, lecture room, Maskingränd 2, Linsen
Starts: 14 February, 2019, 13:15
Ends: 14 February, 2019, 14:15

Published: Fri 08 Feb 2019.