POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Thu 15 Jan 2026 14:25 - 14:50 at Nef - Proof Assistants Chair(s): Dmitriy Traytel

We prove canonicity for a Martin-Löf type theory with a countable universe hierarchy where each universe supports indexed inductive-recursive (IIR) types. We proceed in two steps. First, we construct IIR types from inductive-recursive (IR) types and other basic type formers, in order to simplify the subsequent canonicity proof. The constructed IIR types support the same definitional computation rules that are available in Agda's native IIR implementation. Second, we give a canonicity proof for IR types, building on the established method of gluing along the global sections functor. The main idea is to encode the canonicity predicate for each IR type using a metatheoretic IIR type.

Thu 15 Jan

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

14:00 - 15:40
Proof AssistantsPOPL at Nef
Chair(s): Dmitriy Traytel University of Copenhagen
14:00
25m
Talk
A Lazy, Concurrent Convertibility Checker
POPL
Nathanaëlle Courant OCamlPro, Xavier Leroy Collège de France - PSL University
DOI
14:25
25m
Talk
Canonicity for Indexed Inductive-Recursive Types
POPL
András Kovács University of Gothenburg and Chalmers University of Technology
DOI
14:50
25m
Talk
Coco: Corecursion with Compositional Heterogeneous Productivity
POPL
Jaewoo Kim Seoul National University, Yeonwoo Nam Seoul National University, Chung-Kil Hur Seoul National University
DOI
15:15
25m
Talk
Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation
POPL
Marcus Rossel Barkhausen Institut; TU Darmstadt, Rudi Schneider TU Berlin, Thomas Koehler ICube Lab - CNRS - Université de Strasbourg, Michel Steuwer TU Berlin, Andrés Goens TU Darmstadt
DOI Pre-print