Write a Blog >>
Mon 20 Jan 2020 17:12 - 17:34 at Maurepas - Homotopy Type Theory and PC chairs' report Chair(s): Floris van Doorn

Ordinals and ordinal notation systems play an important role in program verification, since they can be used to prove termination of programs. We present three ordinal notation systems representing ordinals below $\varepsilon_0$ in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. As case studies, we show how basic ordinal arithmetic can be developed for these systems, and how they admit a transfinite induction principle. We prove that all three notation systems are equivalent, so that we can transport results between them using the univalence principle. All our constructions have been implemented in cubical Agda.

Slides (ordinals_cpp.pdf)2.19MiB

Mon 20 Jan

Displayed time zone: Saskatchewan, Central America change

16:50 - 17:56
Homotopy Type Theory and PC chairs' reportCPP at Maurepas
Chair(s): Floris van Doorn University of Pittsburgh
16:50
22m
Talk
Cubical Synthetic Homotopy Theory
CPP
Anders Mörtberg Department of Mathematics, Stockholm University, Loïc Pujet Gallinette Project-Team, Inria
DOI Pre-print Media Attached File Attached
17:12
22m
Talk
Three equivalent ordinal notation systems in Cubical Agda
CPP
Fredrik Nordvall Forsberg University of Strathclyde, Chuangjie Xu Ludwig-Maximilians-Universität München, Neil Ghani University of Strathclyde
DOI Pre-print Media Attached File Attached
17:34
22m
Talk
PC Chairs' report
CPP
Jasmin Blanchette Vrije Universiteit Amsterdam, Cătălin Hriţcu Inria Paris
DOI Media Attached File Attached