Type-theoretic approaches to ordinals (Q2700785): Difference between revisions

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