LFCS Seminar: 4 February 2020 - Fredrik Nordvall Forsberg Title: Ordinal Notation Systems for Ordinals below ε₀ in modern type theories Abstract: Ordinals and well-ordered sets have many applications for reasoning about programs and their termination. For representing ordinals in a computer, one needs a so-called notation system, where each term of the system denotes an ordinal. However, many notation system do not represent ordinals uniquely, which means that e.g. transfinite induction is not provable for the notation system. In contrast, I will present multiple ordinal notation systems uniquely representing ordinals, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. By proving the different systems equivalent, we can transport constructions such as arithmetic operations and properties such as transfinite induction between them using the univalence principle. This is joint work with Chuangjie Xu and Nicolai Kraus. Affiliation: Mathematically Structured Programming Group at the Department of Computer & Information Sciences, University of Strathclyde. Feb 04 2020 16.00 - 17.03 LFCS Seminar: 4 February 2020 - Fredrik Nordvall Forsberg Speaker: Fredrik Nordvall Forsberg Informatics Forum G.03
LFCS Seminar: 4 February 2020 - Fredrik Nordvall Forsberg Title: Ordinal Notation Systems for Ordinals below ε₀ in modern type theories Abstract: Ordinals and well-ordered sets have many applications for reasoning about programs and their termination. For representing ordinals in a computer, one needs a so-called notation system, where each term of the system denotes an ordinal. However, many notation system do not represent ordinals uniquely, which means that e.g. transfinite induction is not provable for the notation system. In contrast, I will present multiple ordinal notation systems uniquely representing ordinals, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. By proving the different systems equivalent, we can transport constructions such as arithmetic operations and properties such as transfinite induction between them using the univalence principle. This is joint work with Chuangjie Xu and Nicolai Kraus. Affiliation: Mathematically Structured Programming Group at the Department of Computer & Information Sciences, University of Strathclyde. Feb 04 2020 16.00 - 17.03 LFCS Seminar: 4 February 2020 - Fredrik Nordvall Forsberg Speaker: Fredrik Nordvall Forsberg Informatics Forum G.03
Feb 04 2020 16.00 - 17.03 LFCS Seminar: 4 February 2020 - Fredrik Nordvall Forsberg Speaker: Fredrik Nordvall Forsberg