Mário Florido, professor at Faculdade de Ciências da Universidade do Porto, is giving a talk at LASIGE on the relation between gradual typing and intersection types. The talk will take place on room C6.2.38, on the 27th of September, at 14h.

This talk is sponsored by LASIGE, under the project UID/CEC/00408/2019.

Título: Gradual Typing and on its Relation with Intersection Types

Abstract:

Gradual typing integrates dynamic and static types. Since its introduction, it has been successfully applied to several extensions of the Simple Type System, including systems with subtyping and parametric polymorphism. We will present a survey of the area of gradual types and recent research about its application to intersection type systems. We present a new approach to define a gradual version of the original intersection type system of Coppo and Dezani. We then present a new operational semantics for terms typed with static and dynamic intersection types, which enables dynamic type casts and identifies the causes for type errors in a framework inspired by the blame calculus. Finally we will talk about a correctness criteria for gradual type systems.

Bio:

Mário Florido is a researcher at LIACC (Laboratório de Inteligência Artificial e Ciência de Computadores da Universidade do Porto) in the area of static analysis and types since 1993. He is also Associate Professor at Faculdade de Ciências da Universidade do Porto where he has been teaching courses mostly related with compilers, semantics of programming languages and functional programming. His main recent research interests include gradual types for functional languages and linear types for extensions of the lambda-calculus with explicit iterators and recursors.