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.
Partially supported by Ministerio de Educación y Ciencia, project MTM2009-13842-C02-01, and by European Community FP7, STREP project ForMath.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Andrés, M., Lambán, L., Rubio, J., Ruiz-Reina, J.L.: Formalizing Simplicial Topology in ACL2. In: Proceedings ACL2 Workshop 2007, pp. 34–39. University of Austin (2007)
Aransay, J., Ballarin, C., Rubio, J.: A mechanized proof of the Basic Perturbation Lemma. Journal of Automated Reasoning 40(4), 271–292 (2008)
Aransay, J., Ballarin, C., Rubio, J.: Generating certified code from formal proofs: a case study in homological algebra. Formal Aspects of Computing 22(2), 193–213 (2010)
Dousson, X., Sergeraert, F., Siret, Y.: The Kenzo program. Institut Fourier, Grenoble (1998), http://www-fourier.ujf-grenoble.fr/~sergerar/Kenzo
Heras, J.: ACL2 verification of Kenzo simplicial sets (2010), http://www.unirioja.es/cu/joheras/ss-tool.html
Heras, J., Pascual, V., Rubio, J.: Using Open Mathematical Documents to interface Computer Algebra and Proof Assistant systems. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) MKM 2009, Held as Part of CICM 2009. LNCS, vol. 5625, pp. 467–473. Springer, Heidelberg (2009)
Kaufmann, M., Moore, J.S.: ACL2 Home Page, http://www.cs.utexas.edu/users/moore/acl2/
Lambán, L., Pascual, V., Rubio, J.: An object-oriented interpretation of the EAT system. Applicable Algebra in Engineering, Communication and Computing 14(3), 187–215 (2003)
Martín-Mateos, F.J., Alonso, J.A., Hidalgo, M.J., Ruiz-Reina, J.L.: A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory. In: Proceedings of the Third ACL2 Workshop, pp. 188–203. University of Grenoble, France (2002)
Martín-Mateos, F.J., Rubio, J., Ruiz-Reina, J.L.: ACL2 verification of simplicial degeneracy programs in the kenzo system. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) MKM 2009, Held as Part of CICM 2009. LNCS, vol. 5625, pp. 106–121. Springer, Heidelberg (2009)
May, J.P.: Simplicial objects in Algebraic Topology. Van Nostrand Mathematical Studies, vol. 11 (1967)
Rubio, J., Sergeraert, F., Siret, Y.: EAT: Symbolic Software for Effective Homology Computation. Institut Fourier, Grenoble (1990), http://www-fourier.ujf-grenoble.fr/~sergerar/Kenzo/#Eat
Sergeraert, F.: The computability problem in Algebraic Topology. Advances in Mathematics 104, 1–29 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Heras, J., Pascual, V., Rubio, J. (2011). Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System. In: Alpuente, M. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2010. Lecture Notes in Computer Science, vol 6564. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20551-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-20551-4_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20550-7
Online ISBN: 978-3-642-20551-4
eBook Packages: Computer ScienceComputer Science (R0)