ETA-RULES IN MARTIN-LÖF TYPE THEORY (Q5240810): Difference between revisions

@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2963738827
@@ Property / OpenAlex ID: W2963738827 / rank @@
+Normal rank
@@ Property / cites work @@
+Do-it-yourself type theory
@@ Property / cites work: Do-it-yourself type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Conditionally reversible computations and weak universality in category theory
+Normal rank
@@ Property / cites work @@
+Combinatory logic. With two sections by William Craig.
+Normal rank
@@ Property / cites work @@
+Identity of Proofs Based on Normalization and Generality
+Normal rank
@@ Property / cites work @@
+Q2724040
@@ Property / cites work: Q2724040 / rank @@
+Normal rank
@@ Property / cites work @@
+Inductive families
@@ Property / cites work: Inductive families / rank @@
+Normal rank
@@ Property / cites work @@
+A general formulation of simultaneous inductive-recursive definitions in type theory
+Normal rank
@@ Property / cites work @@
+On the strength of dependent products in the type theory of Martin-Löf
+Normal rank
@@ Property / cites work @@
+Recursive number theory. A development of recursive arithmetic in a logic-free equation calculus
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / 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 @@
+Extensional Constructs in Intensional Type Theory
@@ Property / cites work: Extensional Constructs in Intensional Type Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q4247303
@@ Property / cites work: Q4247303 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3727946
@@ Property / cites work: Q3727946 / rank @@
+Normal rank
@@ Property / cites work @@
+The Mechanical Evaluation of Expressions
@@ Property / cites work: The Mechanical Evaluation of Expressions / rank @@
+Normal rank
@@ Property / cites work @@
+Q4296744
@@ Property / cites work: Q4296744 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4099614
@@ Property / cites work: Q4099614 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4099613
@@ Property / cites work: Q4099613 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3328540
@@ Property / cites work: Q3328540 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3688389
@@ Property / cites work: Q3688389 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999860
@@ Property / cites work: Q3999860 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2753183
@@ Property / cites work: Q2753183 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4704206
@@ Property / cites work: Q4704206 / rank @@
+Normal rank
@@ Property / cites work @@
+A judgmental reconstruction of modal logic
@@ Property / cites work: A judgmental reconstruction of modal logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q5632554
@@ Property / cites work: Q5632554 / rank @@
+Normal rank
@@ Property / cites work @@
+A natural extension of natural deduction
@@ Property / cites work: A natural extension of natural deduction / rank @@
+Normal rank
@@ Property / cites work @@
+Q3024853
@@ Property / cites work: Q3024853 / rank @@
+Normal rank
@@ Property / cites work @@
+λ-definable functionals andβη conversion
@@ Property / cites work: λ-definable functionals andβη conversion / rank @@
+Normal rank
@@ Property / cites work @@
+Intensional interpretations of functionals of finite type I
+Normal rank
@@ Property / cites work @@
+Primitive Recursive Arithmetic and Its Role in the Foundations of Arithmetic: Historical and Philosophical Reflections
+Normal rank
@@ Property / cites work @@
+Proof-theoretic harmony: towards an intensional account
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:5240810