POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Fri 24 Jan 2025 11:20 - 11:40 at Peek-A-Boo - Types 2

Many programming languages need to check whether two recursive types are in a subtyping relation. Traditionally recursive types are modelled in two different ways: equi- or iso- recursive types. While efficient algorithms for subtyping equi-recursive types are well studied for simple type systems, efficient algorithms for iso-recursive subtyping remain understudied. In this paper we present QuickSub: an efficient and simple to implement algorithm for iso-recursive subtyping. QuickSub has the same expressive power as the well-known iso-recursive Amber rules. The worst case complexity of QuickSub is $O(nm)$, where $m$ is the size of the type and $n$ is the number of recursive binders. However, in practice, the algorithm is nearly linear with the worst case being hard to reach. Consequently, in many common cases, QuickSub can be several times faster than alternative algorithms. We validate the efficiency of QuickSub with an empirical evaluation comparing it to existing equi-recursive and iso-recursive subtyping algorithms. We prove the correctness of the algorithm and formalize a simple calculus with recursive subtyping and records. For this calculus we also show how type soundness can be proved using QuickSub. All the results have been formalized and proved in the Coq proof assistant.

This program is tentative and subject to change.

Fri 24 Jan

Displayed time zone: Mountain Time (US & Canada) change

10:40 - 12:00
Types 2POPL at Peek-A-Boo
10:40
20m
Paper
Affect: An Affine Type and Effect System
POPL
Orpheas van Rooij University of Edinburgh, Robbert Krebbers Radboud University Nijmegen
Link to publication
11:00
20m
Talk
A modal deconstruction of Löb induction
POPL
Daniel Gratzer Aarhus University
11:20
20m
Talk
QuickSub: Efficient Iso-Recursive Subtyping
POPL
Litao Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
11:40
20m
Talk
Generic Refinement Types
POPL