When Subtyping Constraints Liberate: Polymorphic Subtype Inference And Scope Safety

Add to your list(s) Download to your calendar using vCal

• Lionel Parreaux, HKUST (Hong Kong University of Science and Technology)
• Friday 26 January 2024, 15:15-16:15
• SS03, Computer Laboratory.

If you have a question about this talk, please contact Alan Mycroft.

Today we have two Logic and Semantics talks, with a small gap for coffee in between.

Type inference in the presence of first-class or “impredicative” second-order polymorphism à la System F has been an active research area for several decades, with original works dating back to the end of the 80s. Yet, previous solutions to this problem have been quite limited in power and flexibility. For example, it was not clear how to type check expressions like (𝜆𝑥. (𝑥 123, 𝑥 True)) id reliably. This talk introduces SuperF, a new approach based on multi-bounded polymorphism, a form of implicit polymorphic subtyping with multiple upper and lower bounds. SuperF significantly improves on the state of the art in type inference for first-class polymorphism while remaining relatively simple and regular. This talk also discusses a practical implementation of SuperF in the MLscript programming language, together with the existing approach of Boolean-algebraic type inference, and suggests applications in statically guaranteeing the scope safety properties of various programming constructs.

Bio: Lionel Parreaux is an Assistant Professor at HKUST (The Hong Kong University of Science and Technology) since February 2021. He works primarily on type systems, programming language design, and compilers. Together with his research team, the TACO Lab, he is developing the MLscript programming language. He obtained his PhD in 2020 from EPFL , in the Data Analysis Theory and Applications Laboratory (DATA), where he created the Squid type- and scope-safe metaprogramming library for Scala.

This talk is part of the Computer Laboratory Programming Research Group Seminar series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Programming Research Group Seminar
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.