[POPL'26] Canonicity for Indexed Inductive-Recursive Types скачать в хорошем качестве

[POPL'26] Canonicity for Indexed Inductive-Recursive Types

Canonicity for Indexed Inductive-Recursive Types (Video, POPL 2026) András Kovács (University of Gothenburg, Sweden / Chalmers University of Technology, Sweden) Abstract: 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. Article: https://doi.org/10.1145/3776685 ORCID: https://orcid.org/0000-0002-6375-9781 Video Tags: inductive-recursive types, canonicity, doi:10.1145/3776685, orcid:0000-0002-6375-9781 Presentation at the POPL 2026 conference, Jan 11-17, 2026, https://popl26.sigplan.org/ Sponsored by ACM SIGPLAN.