ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System

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

Mathematics Subject Classification ID

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

• ACL2
• Kenzo
• LISP
• EAT

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