Normalisation for First-Class Universe Levels (POPL 2026 - POPL Research Papers)

Sun 11 - Sat 17 January 2026 Rennes, France

Who

Nils Anders Danielsson, Naïm Camille Favier, Ondřej Kubánek

Track

POPL 2026

Time Zone

The program is currently displayed in (GMT+01:00) Brussels, Copenhagen, Madrid, Paris.

Use conference time zone: (GMT+01:00) Brussels, Copenhagen, Madrid, ParisSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Fri 16 Jan 2026 15:15 - 15:40 at Réfectoire - Proof Assistants 2 Chair(s): Matthieu Sozeau

DOI

https://doi.org/10.1145/3776645

Nils Anders Danielsson

University of Gothenburg

Sweden

Naïm Camille Favier

Chalmers University of Technology and University of Gothenburg

Sweden

Ondřej Kubánek

Chalmers University of Technology

Sweden

Time Zone

The program is currently displayed in (GMT+01:00) Brussels, Copenhagen, Madrid, Paris.

Use conference time zone: (GMT+01:00) Brussels, Copenhagen, Madrid, ParisSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

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