Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System
- Heras, J. 1
- Pascual, V. 1
- Rubio, J. 1
-
1
Universidad de La Rioja
info
ISSN: 0302-9743
Year of publication: 2011
Volume: 6564 LNCS
Pages: 37-51
Type: Article
More publications in: Lecture Notes in Computer Science
Abstract
Kenzo is a Common Lisp system devoted to Algebraic Topology. Although Kenzo uses higher-order functional programming intensively, we show in this paper how the theorem prover ACL2 can be used to prove the correctness of first order fragments of Kenzo. More concretely, we report on the verification in ACL2 of the implementation of simplicial sets. By means of a generic instantiation mechanism, we achieve the reduction of the proving effort for each family of simplicial sets, letting ACL2 automate the routine parts of the proofs. © 2011 Springer-Verlag.