POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Fri 16 Jan 2026 10:55 - 11:20 at Réfectoire - Types 2 Chair(s): Amal Ahmed

Quotient types increase the power of type systems by allowing types to include equational properties. However, two key practical issues arise: code being duplicated, and valid code being rejected. Specifically, function definitions often need to be repeated for each quotient of a type, and valid functions may be rejected if they include subterms that do not respect the quotient. This article addresses these reusability and expressivity issues by introducing a notion of quotient polymorphism that we call \emph{choice polymorphism}. We give practical examples of its use, develop the underlying theory, and implement it in Quotient Haskell.

Fri 16 Jan

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

10:30 - 12:10
Types 2POPL at Réfectoire
Chair(s): Amal Ahmed Northeastern University, USA
10:30
25m
Talk
Di- is for Directed: First-Order Directed Type Theory via Dinaturality
POPL
Andrea Laretto Tallinn University of Technology, Fosco Loregian Tallinn University of Technology, Niccolò Veltri IT University of Copenhagen
DOI
10:55
25m
Talk
Quotient PolymorphismDistinguished Paper
POPL
Brandon Hewer , Graham Hutton University of Nottingham
DOI
11:20
25m
Talk
The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types
POPL
Chun Yin Chau HKUST (The Hong Kong University of Science and Technology), Lionel Parreaux Hong Kong University of Science and Technology
DOI
11:45
25m
Talk
Welterweight Go: Boxing, Structural Subtyping, and Generics
POPL
Raymond Hu Queen Mary University of London, Julien Lange Royal Holloway University of London, Bernardo Toninho Instituto Superior Técnico - University of Lisbon, Philip Wadler University of Edinburgh, Robert Griesemer Google, Keith Randall Google
DOI