The Essence of Gradual Typing
Decanato - Facoltà di scienze informatiche
Data: 20 Settembre 2018 / 15:30 - 16:30
USI Lugano Campus, room SI-004, Informatics building (Via G. Buffi 13)
|
|||||||||||
|
|||||||||||
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. 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. |
|||||||||||
|
|||||||||||
Biography: | |||||||||||
É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. |
|||||||||||
|
|||||||||||
|