Pages that link to "Item:Q5428258"
From MaRDI portal
The following pages link to Towards Constructive Homological Algebra in Type Theory (Q5428258):
Displaying 18 items.
- Kenzo (Q17016) (← links)
- Effective homology of bicomplexes, formalized in Coq (Q631755) (← links)
- A mechanized proof of the basic perturbation lemma (Q928666) (← links)
- Generating certified code from formal proofs: a case study in homological algebra (Q968307) (← links)
- \(MP\)-algebras with relative types (Q1272216) (← links)
- Formalization of a normalization theorem in simplicial topology (Q1926582) (← links)
- Higher inductive types as homotopy-initial algebras (Q2819787) (← links)
- Pro-algebraic homotopy types (Q3525978) (← links)
- Proof Pearl: Revisiting the Mini-rubik in Coq (Q3543668) (← links)
- ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System (Q3637272) (← links)
- (Q3719794) (← links)
- Coherent and Strongly Discrete Rings in Type Theory (Q4916066) (← links)
- (Q4944848) (← links)
- Homotopy Type Theory: A synthetic approach to higher equalities (Q5040166) (← links)
- (Q5091143) (← links)
- Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems (Q5505507) (← links)
- Univalent categories of modules (Q6149909) (← links)
- Topological quantum gates in homotopy type theory (Q6584358) (← links)