Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System
From MaRDI portal
Publication:3003483
DOI10.1007/978-3-642-20551-4_3zbMath1326.68261OpenAlexW1847528365MaRDI QIDQ3003483
Vico Pascual, Jónathan Heras, Julio Jesús Rubio García
Publication date: 27 May 2011
Published in: Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-20551-4_3
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
Formalization of a normalization theorem in simplicial topology ⋮ Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials ⋮ Modelling algebraic structures and morphisms in ACL2
Uses Software
Cites Work
- Unnamed Item
- A mechanized proof of the basic perturbation lemma
- Generating certified code from formal proofs: a case study in homological algebra
- The computability problem in algebraic topology
- An object-oriented interpretation of the EAT system
- ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
- Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems
This page was built for publication: Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System
