The Essence of Gradual Typing
Professor Éric Tanter, University of Chile
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.
ES51, lecture room, Maskingränd 2, Linsen
14 February, 2019, 13:15
14 February, 2019, 14:15