Cubical Agda: A dependently typed programming language with univalence and higher inductive types (Q5016211): Difference between revisions

@@ Property / describes a project that uses @@
+Idris
@@ Property / describes a project that uses: Idris / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HoTTSQL
@@ Property / describes a project that uses: HoTTSQL / 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 @@
+Agda
@@ Property / describes a project that uses: Agda / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Lean
@@ Property / describes a project that uses: Lean / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Cubical agda
@@ Property / describes a project that uses: Cubical agda / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+RedPRL
@@ Property / describes a project that uses: RedPRL / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Copatterns
@@ Property / cites work: Copatterns / rank @@
+Normal rank
@@ Property / cites work @@
+Non-wellfounded trees in Homotopy Type Theory
@@ Property / cites work: Non-wellfounded trees in Homotopy Type Theory / rank @@
+Normal rank
@@ Property / cites work @@
+The Integers as a Higher Inductive Type
@@ Property / cites work: The Integers as a Higher Inductive Type / rank @@
+Normal rank
@@ Property / cites work @@
+Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
+Normal rank
@@ Property / cites work @@
+Homotopical patch theory
@@ Property / cites work: Homotopical patch theory / rank @@
+Normal rank
@@ Property / cites work @@
+Guarded cubical type theory
@@ Property / cites work: Guarded cubical type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Idris, a general-purpose dependently typed programming language: Design and implementation
+Normal rank
@@ Property / cites work @@
+Elaborating dependent (co)pattern matching: No pattern left behind
+Normal rank
@@ Property / cites work @@
+Cubical Type Theory: a constructive interpretation of the univalence axiom
+Normal rank
@@ Property / cites work @@
+Refinements for Free!
@@ Property / cites work: Refinements for Free! / rank @@
+Normal rank
@@ Property / cites work @@
+Isomorphism is equality
@@ Property / cites work: Isomorphism is equality / rank @@
+Normal rank
@@ Property / cites work @@
+On Higher Inductive Types in Cubical Type Theory
@@ Property / cites work: On Higher Inductive Types in Cubical Type Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q5089011
@@ Property / cites work: Q5089011 / rank @@
+Normal rank
@@ Property / cites work @@
+Q6079241
@@ Property / cites work: Q6079241 / rank @@
+Normal rank
@@ Property / cites work @@
+The Lean Theorem Prover (System Description)
@@ Property / cites work: The Lean Theorem Prover (System Description) / rank @@
+Normal rank
@@ Property / cites work @@
+The simplicial model of univalent foundations (after Voevodsky)
+Normal rank
@@ Property / cites work @@
+A Cubical Approach to Synthetic Homotopy Theory
@@ Property / cites work: A Cubical Approach to Synthetic Homotopy Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q4993352
@@ Property / cites work: Q4993352 / rank @@
+Normal rank
@@ Property / cites work @@
+Calculating the Fundamental Group of the Circle in Homotopy Type Theory
+Normal rank
@@ Property / cites work @@
+Q4099613
@@ Property / cites work: Q4099613 / rank @@
+Normal rank
@@ Property / cites work @@
+Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract)
+Normal rank
@@ Property / cites work @@
+Q5278410
@@ Property / cites work: Q5278410 / rank @@
+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 @@
+The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory
+Normal rank
@@ Property / cites work @@
+Q5089034
@@ Property / cites work: Q5089034 / rank @@
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory: Univalent Foundations of Mathematics
+Normal rank
@@ Property / cites work @@
+Cubical Agda: A dependently typed programming language with univalence and higher inductive types
+Normal rank
@@ Property / cites work @@
+An experimental library of formalized Mathematics based on the univalent foundations
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1017/s0956796821000034
+Normal rank
@@ Property / OpenAlex ID @@
+W3141612224
@@ Property / OpenAlex ID: W3141612224 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:5016211