When Subtyping Constraints Liberate: Polymorphic Subtype Inference And Scope Safety

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

• 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 nk480.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.