Executing in Common Lisp, Proving in ACL2

DOI10.1007/978-3-540-73086-6_1MaRDI QIDQ5428255zbMATH OpenOpenAlexFDO

Authors Mirian Andrés, Laureano Lambán, Julio Rubio

Publication date 28 November 2007

Published in Towards Mechanized Mathematical Assistants (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73086-6_1

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to algebraic topology (55-04) Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 2101985
• Proving with ACL2 the correctness of simplicial sets in the Kenzo system
• Towards a mechanically checked theory of computation. The ACL2 project
• Applying ACL2 to the formalization of algebraic topology: simplicial polynomials
• An ACL2 Tutorial

Cited in

(6)

• Milestones from the Pure Lisp Theorem Prover to ACL2
• Modelling algebraic structures and morphisms in ACL2
• ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
• Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
• A case-study in algebraic manipulation using mechanized reasoning tools
• Iteration in ACL2

Describes a project that uses

Uses Software

• ACL2
• EAT

This page was built for publication: Executing in Common Lisp, Proving in ACL2

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5428255)