Q5094128 (Q5094128): Difference between revisions

@@ Property / author @@
-Carlo Angiuli
@@ Property / author: Carlo Angiuli / rank @@
-Normal rank
@@ Property / author @@
+Carlo Angiuli
@@ Property / author: Carlo Angiuli / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Propositions as [Types]
@@ Property / cites work: Propositions as [Types] / rank @@
+Normal rank
@@ Property / cites work @@
+Goodwillie's calculus of functors and higher topos theory
+Normal rank
@@ Property / cites work @@
+A generalized Blakers–Massey theorem
@@ Property / cites work: A generalized Blakers–Massey theorem / rank @@
+Normal rank
@@ Property / cites work @@
+Setoid type theory -- a syntactic translation
@@ Property / cites work: Setoid type theory -- a syntactic translation / rank @@
+Normal rank
@@ Property / cites work @@
+Relating first-order set theories, toposes and categories of classes
+Normal rank
@@ Property / cites work @@
+Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
+Normal rank
@@ Property / cites work @@
+A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
+Normal rank
@@ Property / cites work @@
+Computational higher-dimensional type theory
@@ Property / cites work: Computational higher-dimensional type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
+Normal rank
@@ Property / cites work @@
+Topo-logie
@@ Property / cites work: Topo-logie / rank @@
+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 @@
+Q4293501
@@ Property / cites work: Q4293501 / rank @@
+Normal rank
@@ Property / cites work @@
+On Irrelevance and Algorithmic Equality in Predicative Type Theory
+Normal rank
@@ Property / cites work @@
+Homotopy theoretic models of identity types
@@ Property / cites work: Homotopy theoretic models of identity types / rank @@
+Normal rank
@@ Property / cites work @@
+A Brief Introduction to Algebraic Set Theory
@@ Property / cites work: A Brief Introduction to Algebraic Set Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q3575369
@@ Property / cites work: Q3575369 / rank @@
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory
@@ Property / cites work: Homotopy Type Theory / rank @@
+Normal rank
@@ Property / cites work @@
+A cubical model of homotopy type theory
@@ Property / cites work: A cubical model of homotopy type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Natural models of homotopy type theory
@@ Property / cites work: Natural models of homotopy type theory / rank @@
+Normal rank
@@ Property / cites work @@
+A Kripke model for simplicial sets
@@ Property / cites work: A Kripke model for simplicial sets / rank @@
+Normal rank
@@ Property / cites work @@
+Q2968413
@@ Property / cites work: Q2968413 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5591514
@@ Property / cites work: Q5591514 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4304740
@@ Property / cites work: Q4304740 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4314472
@@ Property / cites work: Q4314472 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5387319
@@ Property / cites work: Q5387319 / rank @@
+Normal rank
@@ Property / cites work @@
+Programming with algebraic effects and handlers
@@ Property / cites work: Programming with algebraic effects and handlers / rank @@
+Normal rank
@@ Property / cites work @@
+Generalized algebraic theories and contextual categories
+Normal rank
@@ Property / cites work @@
+Cubical Type Theory: a constructive interpretation of the univalence axiom
+Normal rank
@@ Property / cites work @@
+The biequivalence of locally cartesian closed categories and Martin-Löf type theories
+Normal rank
@@ Property / cites work @@
+Q5089011
@@ Property / cites work: Q5089011 / rank @@
+Normal rank
@@ Property / cites work @@
+Connected limits, familial representability and Artin glueing
+Normal rank
@@ Property / cites work @@
+Q4012882
@@ Property / cites work: Q4012882 / rank @@
+Normal rank
@@ Property / cites work @@
+An algorithm for type-checking dependent types
@@ Property / cites work: An algorithm for type-checking dependent types / rank @@
+Normal rank
@@ Property / cites work @@
+Type theory and formalisation of mathematics
@@ Property / cites work: Type theory and formalisation of mathematics / rank @@
+Normal rank
@@ Property / cites work @@
+Canonicity and normalization for dependent type theory
+Normal rank
@@ Property / cites work @@
+The Type Theory of PL/CV3
@@ Property / cites work: The Type Theory of PL/CV3 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4263868
@@ Property / cites work: Q4263868 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5625124
@@ Property / cites work: Q5625124 / rank @@
+Normal rank
@@ Property / cites work @@
+Constructing type systems over an operational semantics
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Q4225149
@@ Property / cites work: Q4225149 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3204055
@@ Property / cites work: Q3204055 / rank @@
+Normal rank
@@ Property / cites work @@
+On equivalence and canonical forms in the LF type theory
+Normal rank
@@ Property / cites work @@
+Q4247303
@@ Property / cites work: Q4247303 / rank @@
+Normal rank
@@ Property / cites work @@
+Canonicity for cubical type theory
@@ Property / cites work: Canonicity for cubical type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q4281477
@@ Property / cites work: Q4281477 / rank @@
+Normal rank
@@ Property / cites work @@
+Pointers in Recursion: Exploring the Tropics
@@ Property / cites work: Pointers in Recursion: Exploring the Tropics / rank @@
+Normal rank
@@ Property / cites work @@
+Type theory in type theory using quotient inductive types
+Normal rank
@@ Property / cites work @@
+The simplicial model of univalent foundations (after Voevodsky)
+Normal rank
@@ Property / cites work @@
+FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
@@ Property / cites work: FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES / rank @@
+Normal rank
@@ Property / cites work @@
+Weak omega-categories from intensional type theory
+Normal rank
@@ Property / cites work @@
+Higher Topos Theory (AM-170)
@@ Property / cites work: Higher Topos Theory (AM-170) / 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 @@
+Q4215784
@@ Property / cites work: Q4215784 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4283246
@@ Property / cites work: Q4283246 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999860
@@ Property / cites work: Q3999860 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5278410
@@ Property / cites work: Q5278410 / rank @@
+Normal rank
@@ Property / cites work @@
+A Verified Theorem Prover Backend Supported by a Monotonic Library
+Normal rank
@@ Property / cites work @@
+A type theory for synthetic $\infty$-categories
@@ Property / cites work: A type theory for synthetic $\infty$-categories / rank @@
+Normal rank
@@ Property / cites work @@
+Q5089034
@@ Property / cites work: Q5089034 / rank @@
+Normal rank
@@ Property / cites work @@
+Deciding type equivalence in a language with singleton kinds
+Normal rank
@@ Property / cites work @@
+Extensional equivalence and singleton types
@@ Property / cites work: Extensional equivalence and singleton types / rank @@
+Normal rank
@@ Property / cites work @@
+Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
+Normal rank
@@ Property / cites work @@
+The univalence axiom for elegant Reedy presheaves
@@ Property / cites work: The univalence axiom for elegant Reedy presheaves / rank @@
+Normal rank
@@ Property / cites work @@
+Univalence for inverse diagrams and homotopy canonicity
+Normal rank
@@ Property / cites work @@
+Q5718564
@@ Property / cites work: Q5718564 / rank @@
+Normal rank
@@ Property / cites work @@
+A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
+Normal rank
@@ Property / cites work @@
+Programming up to Congruence
@@ Property / cites work: Programming up to Congruence / rank @@
+Normal rank
@@ Property / cites work @@
+Intensional interpretations of functionals of finite type I
+Normal rank
@@ Property / cites work @@
+Q4243759
@@ Property / cites work: Q4243759 / rank @@
+Normal rank
@@ Property / cites work @@
+Constructivism in mathematics. An introduction. Volume I
+Normal rank
@@ Property / cites work @@
+Fibred Fibration Categories
@@ Property / cites work: Fibred Fibration Categories / rank @@
+Normal rank
@@ Property / cites work @@
+Q5091148
@@ Property / cites work: Q5091148 / rank @@
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory: Univalent Foundations of Mathematics
+Normal rank
@@ Property / cites work @@
+Types are weak <i>ω</i> -groupoids
@@ Property / cites work: Types are weak <i>ω</i> -groupoids / rank @@
+Normal rank
@@ Property / cites work @@
+Cubical Agda: A dependently typed programming language with univalence and higher inductive types
+Normal rank
@@ Property / cites work @@
+Homotopy theory of simplicial sheaves in completely decomposable topologies
+Normal rank
@@ Property / cites work @@
+Subsystems and regular quotients of C-systems
@@ Property / cites work: Subsystems and regular quotients of C-systems / rank @@
+Normal rank