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

This program is tentative and subject to change.

Wed 14 Jan 2026 14:25 - 14:50 at Nef - Types 1

Recent research has demonstrated the effectiveness of extending the Hindley-Milner (HM) type system with Boolean kinds to support type inference for a wide variety of features. However, the means to support classic type system provisions such as local let generalization and polymorphic recursion is either limited or unknown for such extensions. This paper contributes procedures for equational generalization and semiunification in arbitrary Boolean rings, enabling let generalization and polymorphic recursion in Boolean-kinded type inference. Additionally, methods to minimize the number of bound Boolean type variables are developed to keep types small in these systems. Boolean-kinded HM extensions are exemplified with \textit{nullable reference types}, and how to use the developed procedures to support let generalization and polymorphic recursion is outlined.

This program is tentative and subject to change.

Wed 14 Jan

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

14:00 - 15:40
Types 1POPL at Nef
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