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

Strictness analysis is critical to efficient implementation of languages with non-strict evaluation, mitigating much of the performance overhead of laziness. However, reasoning about strictness at the source level can be challenging and unintuitive. We propose a new definition of strictness that refines the traditional one by describing variable usage more precisely. We lay type-theoretic foundations for this definition in both call-by-name and call-by-push-value settings, drawing inspiration from the literature on type systems tracking effects and coeffects. We prove via a logical relation that the strictness attributes computed by our type systems accurately describe the use of variables at runtime, and we offer a strictness-annotation-preserving translation from the call-by-name system to the call-by-push-value one. All our results are mechanized in Rocq.

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