POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France

This program is tentative and subject to change.

Sat 17 Jan 2026 17:00 - 17:22 at Salle 13 - Session 4

Type narrowing is the central innovation that makes gradual typing work for languages such as JavaScript and Python. To quote John Reynolds (1968), narrowing uses the “premises in conditional expressions” to refine the types of variables and data structures. But exactly how to use the premises is up for debate. Nearly every gradual typechecker supports basic type narrowing, but after analyzing eight typecheckers in depth we have yet to find two that fully agree on the details! This talk will present the dimensions of type narrowing, the pitfalls of simple implementation strategies, and the mechanics of the effective but “hard” strategy of occurrence typing as found in Typed Racket and Typed Clojure.

This program is tentative and subject to change.

Sat 17 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

16:00 - 18:00
Session 4WITS at Salle 13
16:00
40m
Keynote
Verifying Dependent Type-checkers
WITS
Meven Lennon-Bertrand Inria – Université Paris Cité
17:00
22m
Talk
Type Narrowing the Hard Way
WITS
Ben Greenman University of Utah, Hanwen Guo University of Utah
17:23
2m
Other
Closing
WITS
Niki Vazou IMDEA Software Institute