QuickSub: Efficient Iso-Recursive Subtyping

This video presents a research talk from POPL 2025 introducing QuickSub, an efficient algorithm for iso-recursive subtyping. Learn about this novel approach developed by researchers Litao Zhou and Bruno C. d. S. Oliveira from the University of Hong Kong that addresses a gap in efficient algorithms for iso-recursive subtyping. Discover how QuickSub matches the expressive power of the Amber rules while achieving better performance with O(nm) worst-case complexity that performs nearly linearly in practice. The presentation covers the algorithm's design, correctness proofs formalized in Coq, and empirical evaluations showing QuickSub outperforming existing approaches. Access supplementary materials including the paper, code repository, and artifacts that have been evaluated as functional. This 20-minute talk is ideal for programming language researchers and developers interested in type systems, recursive types, and subtyping algorithms.