Type-theoretic approaches to ordinals

DOI10.1016/j.tcs.2023.113843OpenAlexW4360977267MaRDI QIDQ2700785

Nicolai Kraus, Chuangjie Xu, Fredrik Nordvall Forsberg

Publication date: 27 April 2023

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2208.03844

zbMATH Keywords

constructive mathematicsordinal numbershomotopy type theoryBrouwer treesCantor normal formsextensional well-founded orders

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Uses Software

• Coq
• Isabelle/HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proofs, programs, processes
• Ordinal arithmetic: Algorithms and mechanization
• Proof theory. 2nd ed
• A new system of proof-theoretic ordinal functions
• A course in constructive algebra
• Induction-recursion and initial algebras.
• Quotient inductive-inductive types
• A mechanizable first-order theory of ordinals
• Intuitionistic fixed point logic
• Notation systems for infinitary derivations
• Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie
• Kennzeichnung von Ordnungszahlen durch rekursiv erklärte Funktionen
• Cardinals in Isabelle/HOL
• Partiality, Revisited
• Proving termination with multiset orderings
• Semantics of higher inductive types
• A Syntax for Higher Inductive-Inductive Types
• Cubical Agda: A dependently typed programming language with univalence and higher inductive types
• Trees, ordinals and termination
• On Higher Inductive Types in Cubical Type Theory
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Ordinal recursion, and a refinement of the extended Grzegorczyk hierarchy
• Intuitionistic sets and ordinals
• The constructive second number class
• On notation for ordinal numbers
• The consistency of arithmetics