If you do not see this message displayed properly, please click here


The Faculty of Informatics is pleased to announce a seminar given by Éric Tanter 



The Essence of Gradual Typing
Speaker: Éric Tanter
University of Chile & Inria Paris
Date: Thursday, September 20, 2018
Place: USI Lugano Campus, room SI-004, Informatics building (Via G. Buffi 13)
Time: 15:30-16:30



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.


Host: Prof. Matthias Hauswirth


Faculty of Informatics

Faculty of Informatics
Università della Svizzera italiana
Via Giuseppe Buffi 13
CH-6904 Lugano
Tel.: +41 (0)58 666 46 90
Fax: +41 (0)58 666 45 36
Email: decanato.inf@usi.ch
Web: www.inf.usi.ch
Twitter: @USI_INF


Segui USI@EXPO2015 su Twitter Segui USI@EXPO2015 su Facebook Segui USI@EXPO2015 su Linkedin Segui USI@EXPO2015 su YouTube