Cartesian cubical computational type theory: Constructive reasoning with paths and equalities (Q5079726): Difference between revisions

@@ label / en / label / en @@
+Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
@@ Property / author @@
+Carlo Angiuli
@@ Property / author: Carlo Angiuli / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+GitHub
@@ Property / describes a project that uses: GitHub / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+cubicaltt
@@ Property / describes a project that uses: cubicaltt / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+cart-cube
@@ Property / describes a project that uses: cart-cube / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Innovations in computational type theory using Nuprl
+Normal rank
@@ Property / cites work @@
+Q5278407
@@ Property / cites work: Q5278407 / rank @@
+Normal rank
@@ Property / cites work @@
+Towards a Formally Verified Proof Assistant
@@ Property / cites work: Towards a Formally Verified Proof Assistant / rank @@
+Normal rank
@@ Property / cites work @@
+Computational higher-dimensional type theory
@@ Property / cites work: Computational higher-dimensional type theory / rank @@
+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 @@
+Q2968413
@@ Property / cites work: Q2968413 / rank @@
+Normal rank
@@ Property / cites work @@
+Varieties of Cubical Sets
@@ Property / cites work: Varieties of Cubical Sets / rank @@
+Normal rank
@@ Property / cites work @@
+Cubical Type Theory: a constructive interpretation of the univalence axiom
+Normal rank
@@ Property / cites work @@
+Constructive mathematics and computer programming
@@ Property / cites work: Constructive mathematics and computer programming / rank @@
+Normal rank
@@ Property / cites work @@
+Q3688389
@@ Property / cites work: Q3688389 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5277978
@@ Property / cites work: Q5277978 / rank @@
+Normal rank
@@ Property / cites work @@
+Intensional interpretations of functionals of finite type I
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory: Univalent Foundations of Mathematics
+Normal rank
@@ Property / cites work @@
+Homotopy type theory in Lean
@@ Property / cites work: Homotopy type theory in Lean / rank @@
+Normal rank
@@ Property / cites work @@
+Homotopy theory of simplicial sheaves in completely decomposable topologies
+Normal rank
@@ Property / full work available at URL @@
+https://dblp.uni-trier.de/db/conf/csl/csl2018.html#AngiuliF018
+Normal rank
@@ Property / OpenAlex ID @@
+W2888798587
@@ Property / OpenAlex ID: W2888798587 / rank @@
+Normal rank
@@ Property / title @@
+Cartesian cubical computational type theory: Constructive reasoning with paths and equalities (English)
+Normal rank