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
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

CPP-2020-papers
16:50 - 17:56: CPP 2020 - Homotopy Type Theory and PC chairs' report at Maurepas
Chair(s): Floris van DoornUniversity of Pittsburgh
CPP-2020-papers16:50 - 17:12
Talk
Anders MörtbergDepartment of Mathematics, Stockholm University, Loïc PujetGallinette Project-Team, Inria
DOI Pre-print Media Attached File Attached
CPP-2020-papers17:12 - 17:34
Talk
Fredrik Nordvall ForsbergUniversity of Strathclyde, Chuangjie XuLudwig-Maximilians-Universität München, Neil GhaniUniversity of Strathclyde
DOI Pre-print Media Attached File Attached
CPP-2020-papers17:34 - 17:56
Talk
Jasmin BlanchetteVrije Universiteit Amsterdam, Cătălin HriţcuInria Paris
DOI Media Attached File Attached