MARTIN-LÖF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK (Q5249247): Difference between revisions

@@ Property / cites work @@
+Do-it-yourself type theory
@@ Property / cites work: Do-it-yourself type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Recursive models for constructive set theories
@@ Property / cites work: Recursive models for constructive set theories / rank @@
+Normal rank
@@ Property / cites work @@
+An intuitionistic theory of types with assumptions of high-arity variables
+Normal rank
@@ Property / cites work @@
+Inductive families
@@ Property / cites work: Inductive families / rank @@
+Normal rank
@@ Property / cites work @@
+Constructing type systems over an operational semantics
+Normal rank
@@ Property / cites work @@
+A NEW FORMALIZATION OF FEFERMAN’S SYSTEM OF FUNCTIONS AND CLASSES AND ITS RELATION TO FREGE STRUCTURE
+Normal rank
@@ Property / cites work @@
+Proving congruence of bisimulation in functional programming languages
+Normal rank
@@ Property / cites work @@
+A TYPE-FREE THEORY OF HALF-MONOTONE INDUCTIVE DEFINITIONS
+Normal rank
@@ Property / cites work @@
+Realizability interpretation of generalized inductive definitions
+Normal rank
@@ Property / cites work @@
+Equational theories for inductive types
@@ Property / cites work: Equational theories for inductive types / rank @@
+Normal rank
@@ Property / cites work @@
+An interpretation of Martin-Löf's type theory in a type-free theory of propositions
+Normal rank
@@ Property / cites work @@
+HYBRID PARTIAL-TOTAL TYPE THEORY
@@ Property / cites work: HYBRID PARTIAL-TOTAL TYPE THEORY / rank @@
+Normal rank
@@ Property / cites work @@
+Reading between the lines in constructive type theory
+Normal rank