ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
From MaRDI portal
Publication:3637272
DOI10.1007/978-3-642-02614-0_13zbMath1247.68325OpenAlexW1605757265MaRDI QIDQ3637272
José Luis Ruiz-Reina, Francisco Jesús Martín-Mateos, Julio Jesús Rubio García
Publication date: 9 July 2009
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-02614-0_13
Symbolic computation and algebraic computation (68W30) Software, source code, etc. for problems pertaining to algebraic topology (55-04)
Related Items (5)
Formalization of a normalization theorem in simplicial topology ⋮ Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System ⋮ Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials ⋮ ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System ⋮ Modelling algebraic structures and morphisms in ACL2
Uses Software
Cites Work
- A mechanized proof of the basic perturbation lemma
- An object-oriented interpretation of the EAT system
- ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
- Computer Aided Systems Theory – EUROCAST 2005
- Executing in Common Lisp, Proving in ACL2
- Towards Constructive Homological Algebra in Type Theory
- Object oriented institutions to specify symbolic computation systems
- Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
- Mediated Access to Symbolic Computation Systems
- Unnamed Item
- Unnamed Item
This page was built for publication: ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
