Abstract
Kenzo is a Computer Algebra system devoted to Algebraic Topology, and written in the Common Lisp programming language. It is a descendant of a previous system called EAT (for Effective Algebraic Topology). Kenzo shows a much better performance than EAT due, among other reasons, to a smart encoding of degeneracy lists as integers. In this paper, we give a complete automated proof of the correctness of this encoding used in Kenzo. The proof is carried out using ACL2, a system for proving properties of programs written in (a subset of) Common Lisp. The most interesting idea, from a methodological point of view, is our use of EAT to build a model on which the verification is carried out. Thus, EAT, which is logically simpler but less efficient than Kenzo, acts as a mathematical model and then Kenzo is formally verified against it.
This work has been supported by Ministerio de Educación y Ciencia, project MTM2006-06513.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Andrés, M., Lambán, L., Rubio, J.: Executing in Common Lisp, Proving in ACL2. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/CALCULEMUS 2007. LNCS, vol. 4573, pp. 1–12. Springer, Heidelberg (2007)
Andrés, M., Lambán, L., Rubio, J., Ruiz-Reina, J.L.: Formalizing Simplicial Topology in ACL2. In: ACL2 Workshop 2007, University of Austin, pp. 34–39 (2007)
Aransay, J., Ballarin, C., Rubio, J.: A Mechanized Proof of the Basic Perturbation Lemma. Journal of Automated Reasoning 40, 271–292 (2008)
Aransay, J., Ballarin, C., Rubio, J.: Extracting Computer Algebra Programs from Statements. In: Moreno Díaz, R., Pichler, F., Quesada Arencibia, A. (eds.) EUROCAST 2005. LNCS, vol. 3643, pp. 159–168. Springer, Heidelberg (2005)
Coquand, T., Spiwack, A.: Towards Constructive Homological Algebra in Type Theory. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/CALCULEMUS 2007. LNCS, vol. 4573, pp. 40–54. Springer, Heidelberg (2007)
Domínguez, C.: Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS, vol. 5144, pp. 270–284. Springer, Heidelberg (2008)
Domínguez, C., Lambán, L., Rubio, J.: Object Oriented Institutions to Specify Symbolic Computation Systems. Rairo - Theoretical Informatics and Applications 41, 191–214 (2007)
Dousson, X., Rubio, J., Sergeraert, F., Siret, Y.: The Kenzo Program, Institut Fourier (1999), http://www-fourier.ujf-grenoble.fr/~sergerar/Kenzo/
Heras, J., Pascual, V., Rubio, J.: Mediated Access to Symbolic Computation Systems. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS, vol. 5144, pp. 446–461. Springer, Heidelberg (2008)
Kaufmann, M., Manolios, P., Moore, J S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)
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, 187–215 (2003)
Martín–Mateos, F.J., Ruiz–Reina, J.L., Rubio, J.: ACL2 verification of simplicial degeneracy programs in the Kenzo system, http://www.cs.us.es/~fmartin/acl2/kenzo
May, J.P.: Simplicial Objects in Algebraic Topology. Van Nostrand (1967)
Rubio, J., Sergeraert, F., Siret, Y.: EAT: Symbolic Software for Effective Homology Computation, Institut Fourier (1997), ftp://ftp-fourier.ujf-grenoble.fr/pub/EAT
Steele Jr., G.L.: Common Lisp The Language, 2nd edn. Digital Press (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Martín-Mateos, FJ., Rubio, J., Ruiz-Reina, JL. (2009). ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds) Intelligent Computer Mathematics. CICM 2009. Lecture Notes in Computer Science(), vol 5625. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02614-0_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-02614-0_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02613-3
Online ISBN: 978-3-642-02614-0
eBook Packages: Computer ScienceComputer Science (R0)