A general formulation of simultaneous inductive-recursive definitions in type theory (Q4508246): Difference between revisions

@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.2307/2586554
@@ Property / full work available at URL: https://doi.org/10.2307/2586554 / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2058174669
@@ Property / OpenAlex ID: W2058174669 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q59540955
@@ Property / Wikidata QID: Q59540955 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5573965
@@ Property / cites work: Q5573965 / rank @@
+Normal rank
@@ Property / cites work @@
+Inaccessibility in constructive set theory and type theory
+Normal rank
@@ Property / cites work @@
+A TYPE-FREE THEORY OF HALF-MONOTONE INDUCTIVE DEFINITIONS
+Normal rank
@@ Property / cites work @@
+Inductive families
@@ Property / cites work: Inductive families / rank @@
+Normal rank
@@ Property / cites work @@
+Normalization and the Yoneda embedding
@@ Property / cites work: Normalization and the Yoneda embedding / rank @@
+Normal rank
@@ Property / cites work @@
+Intuitionistic model constructions and normalization proofs
+Normal rank
@@ Property / cites work @@
+Propositional functions and families of types
@@ Property / cites work: Propositional functions and families of types / rank @@
+Normal rank
@@ Property / cites work @@
+The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:4508246