Recursive types are pervasive in programming languages and compiler infrastructures, from algebraic data types in functional languages to intermediate representations in modern compilers. However, checking subtyping between recursive types remains challenging. Traditional algorithms like Amber rules require backtracking, leading to performance bottlenecks at scale.

This talk is focused on presenting QuickSub, an efficient iso-recursive subtyping algorithm that checks subtyping in a single traversal and exhibits linear-time performance in practice. I will also discuss my other work and future directions in recursive types metatheory and their applications to programming languages.

Topic: HKUPLG Seminar Time: Oct 7, 2026 09:30 AM Hong Kong SAR

Join Zoom Meeting https://hku.zoom.us/j/95231543417?pwd=IJds7cPyRAgbU2b3cIyth6Eda5U11m.1

Meeting ID: 952 3154 3417 Password: 739695