Formalization of a normalization theorem in simplicial topology
From MaRDI portal
Publication:1926582
DOI10.1007/s10472-011-9274-6zbMath1280.68232OpenAlexW2034552599MaRDI QIDQ1926582
Laureano Lambán, Julio Jesús Rubio García, José Luis Ruiz-Reina, Francisco Jesús Martín-Mateos
Publication date: 28 December 2012
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://idus.us.es/handle//11441/86280
Symbolic computation and algebraic computation (68W30) Simplicial sets and complexes in algebraic topology (55U10)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A mechanized proof of the basic perturbation lemma
- Generating certified code from formal proofs: a case study in homological algebra
- Triangulations. Structures for algorithms and applications
- A verified common lisp implementation of Buchberger's algorithm in ACL2
- Sheaves in geometry and logic: a first introduction to topos theory
- An object-oriented interpretation of the EAT system
- Homological perturbation theory and associativity
- Constructive algebraic topology
- Semisimplicial objects and the Eilenberg-Zilber Theorem
- Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System
- Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials
- Computing in Coq with Infinite Algebraic Data Structures
- ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
- Towards Constructive Homological Algebra in Type Theory
- Object oriented institutions to specify symbolic computation systems
