POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Fri 19 Jan 2024 13:40 - 14:00 at Kelvin Lecture - Types 3 Chair(s): Steven Ramsay

We study the interaction of structural subtyping with parametric polymorphism and recursively defined type constructors. Although structural subtyping is undecidable in this setting, we describe a notion of parametricity for type constructors and then exploit it to define parametric subtyping, a conceptually simple, decidable, and expressive fragment of structural subtyping that strictly generalizes nominal subtyping. We present and prove correct an effective saturation-based decision procedure for parametric subtyping, demonstrating its applicability using a variety of examples. An implementation of this decision procedure is available in the supplementary materials.

Fri 19 Jan

Displayed time zone: London change

13:20 - 14:40
Types 3POPL at Kelvin Lecture
Chair(s): Steven Ramsay University of Bristol
13:20
20m
Talk
When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
POPL
Lionel Parreaux HKUST (The Hong Kong University of Science and Technology), Aleksander Boruch-Gruszecki EPFL, Andong Fan HKUST (The Hong Kong University of Science and Technology), Chun Yin Chau HKUST (The Hong Kong University of Science and Technology)
DOI Pre-print Media Attached File Attached
13:40
20m
Talk
Parametric Subtyping for Structural Parametric PolymorphismDistinguished PaperRemote
POPL
Henry DeYoung CMU, Andreia Mordido University of Lisbon, Frank Pfenning Carnegie Mellon University, USA, Ankush Das Amazon
14:00
20m
Talk
Unboxed data constructors -- or, how cpp decides a halting problem
POPL
Nicolas Chataing ENS Paris, Stephen Dolan Jane Street, Gabriel Scherer INRIA Saclay, Jeremy Yallop University of Cambridge
14:20
20m
Talk
Polymorphic Type Inference for Dynamic Languages
POPL
Giuseppe Castagna CNRS; Université Paris Cité, Mickaël Laurent Université Paris Cité / IRIF, Kim Nguyễn Université Paris-Saclay
Link to publication DOI