BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:When Subtyping Constraints Liberate: Polymorphic Subtype Inference
  And Scope Safety -  HKUST (Hong Kong University of Science and Technology
 )
DTSTART:20240126T151500Z
DTEND:20240126T161500Z
UID:TALK211411@talks.cam.ac.uk
CONTACT:47138
DESCRIPTION:Type inference in the presence of first-class or “impredicat
 ive” second-order polymorphism à la System F has been an active researc
 h 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 chec
 k expressions like (𝜆𝑥. (𝑥 123\, 𝑥 True)) id reliably. This ta
 lk introduces SuperF\, a new approach based on multi-bounded polymorphism\
 , a form of implicit polymorphic subtyping with multiple upper and lower b
 ounds. SuperF significantly improves on the state of the art in type infer
 ence for first-class polymorphism while remaining relatively simple and re
 gular. This talk also discusses a practical implementation of SuperF in th
 e MLscript programming language\, together with the existing approach of B
 oolean-algebraic type inference\, and suggests applications in statically 
 guaranteeing the scope safety properties of various programming constructs
 .
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR