Q6079230 (Q6079230): Difference between revisions

@@ Property / cites work @@
+Quotient inductive-inductive types
@@ Property / cites work: Quotient inductive-inductive types / rank @@
+Normal rank
@@ Property / cites work @@
+Big-step normalisation
@@ Property / cites work: Big-step normalisation / rank @@
+Normal rank
@@ Property / cites work @@
+Categorical reconstruction of a reduction free normalization proof
+Normal rank
@@ Property / cites work @@
+Normalisation by Evaluation for Dependent Types.
@@ Property / cites work: Normalisation by Evaluation for Dependent Types. / rank @@
+Normal rank
@@ Property / cites work @@
+Type theory in type theory using quotient inductive types
+Normal rank
@@ Property / cites work @@
+Type Theory Should Eat Itself
@@ Property / cites work: Type Theory Should Eat Itself / rank @@
+Normal rank
@@ Property / cites work @@
+Cubical Type Theory: a constructive interpretation of the univalence axiom
+Normal rank
@@ Property / cites work @@
+Q4012882
@@ Property / cites work: Q4012882 / rank @@
+Normal rank
@@ Property / cites work @@
+Internal type theory
@@ Property / cites work: Internal type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q3994895
@@ Property / cites work: Q3994895 / rank @@
+Normal rank
@@ Property / cites work @@
+A coherence theorem for Martin-Löf's type theory
@@ Property / cites work: A coherence theorem for Martin-Löf's type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q4225149
@@ Property / cites work: Q4225149 / rank @@
+Normal rank
@@ Property / cites work @@
+Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
+Normal rank
@@ Property / cites work @@
+Call-by-push-value: Decomposing call-by-value and call-by-name
+Normal rank
@@ Property / cites work @@
+Q3024846
@@ Property / cites work: Q3024846 / rank @@
+Normal rank
@@ Property / cites work @@
+Intensional interpretations of functionals of finite type I
+Normal rank