POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Fri 16 Jan 2026 14:00 - 14:25 at Réfectoire - Proof Assistants 2 Chair(s): Matthieu Sozeau

The ability to cast values between related types is a leitmotiv of many flavors of dependent type theory, such as observational type theories, subtyping, or cast calculi for gradual typing. These casts all exhibit a common structural behavior that boils down to the pervasive functoriality of type formers. We propose and extensively study a type theory, called AdapTT, which makes systematic and precise this idea of functorial type formers, with respect to an abstract notion of adapters relating types. Leveraging descriptions for functorial inductive types in AdapTT, we derive structural laws for type casts on general inductive type formers.

Fri 16 Jan

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

14:00 - 15:40
Proof Assistants 2POPL at Réfectoire
Chair(s): Matthieu Sozeau Inria
14:00
25m
Talk
AdapTT: Functoriality for Dependent Type Casts
POPL
Arthur Adjedj ENS Paris Saclay, Université Paris-Saclay, Meven Lennon-Bertrand Inria – Université Paris Cité, Thibaut Benjamin Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, Kenji Maillard Inria
DOI
14:25
25m
Talk
Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach
POPL
Yiyun Liu University of Pennsylvania, Stephanie Weirich University of Pennsylvania
DOI
14:50
25m
Talk
Encode the Cake and Eat It Too: Controlling Computation in Type Theory, LocallyDistinguished Paper
POPL
Yann Leray Nantes Université; Inria, Théo Winterhalter INRIA
DOI
15:15
25m
Talk
Normalisation for First-Class Universe LevelsDistinguished PaperRemote
POPL
Nils Anders Danielsson University of Gothenburg, Naïm Camille Favier Chalmers University of Technology and University of Gothenburg, Ondřej Kubánek Chalmers University of Technology
DOI