POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Wed 14 Jan 2026 14:00 - 14:25 at Nef - Types 1 Chair(s): Lionel Parreaux

This paper proposes a novel language design that combines extensible data types, implemented through row types and row polymorphism, with ad-hoc polymorphism, implemented through type classes. Our design introduces several new constructs and constraints useful for generic operations over rows. We formalize our design in a source calculus λ⇒ρ, which elaborates into a target calculus F⊗⊕ω. We prove that the target calculus is type-safe and that the elaboration is sound, thus establishing the soundness of λ⇒ρ. All proofs are mechanized in the Lean 4 proof assistant. Furthermore, we evaluate our type system using the Brown Benchmark for Table Types, demonstrating the utility of extensible rows with type classes for table types.

Wed 14 Jan

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

14:00 - 15:40
Types 1POPL at Nef
Chair(s): Lionel Parreaux Hong Kong University of Science and Technology
14:00
25m
Talk
Extensible Data Types with Ad-Hoc Polymorphism
POPL
Matthew Toohey University of Toronto, Yanning Chen University of Toronto, Ara Jamalzadeh University of Toronto, Ningning Xie University of Toronto
DOI Pre-print
14:25
25m
Talk
Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems
POPL
Joseph Zullo Purdue University
DOI
14:50
25m
Talk
Local Contextual Type Inference
POPL
Xu Xue University of Hong Kong, Chen Cui University of Hong Kong, Shengyi Jiang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI
15:15
25m
Talk
Typing Strictness
POPL
Daniel Sainati University of Pennsylvania, Joseph W. Cutler University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Stephanie Weirich University of Pennsylvania
DOI