Formalization of a normalization theorem in simplicial topology

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

zbMATH Keywords

automated reasoningalgebraic topologyACL2formalization of mathematicsnormalization theorem

Mathematics Subject Classification ID

Related Items (1)

Modelling algebraic structures and morphisms in ACL2

Uses Software

• ACL2
• Kenzo
• EAT

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

This page was built for publication: Formalization of a normalization theorem in simplicial topology