Skip to main content
SpringerLink
Log in

Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems

  • Conference paper
Book cover Intelligent Computer Mathematics (CICM 2008)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 5144))

Included in the following conference series:

Abstract

This work is an attempt to formalize, using the Coq proof assistant, the algebraic specification of the data structures appearing in two symbolic computation systems for algebraic topology called EAT and Kenzo. The specification of these structures have been obtained through an operation, called imp operation, between different specification frameworks as standard algebraic specifications and hidden specifications. Reusing previous Coq implementations of universal algebra and category theory we have proposed a Coq formalization of the imp operation, extending the representation to the particular hidden algebras which take part in this operation.

Partially supported by Ministerio de Educación y Ciencia, project MTM2006-06513.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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 (LNAI), vol. 4573, pp. 1–12. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  2. Aransay, J., Ballarin, C., Rubio, J.: A Mechanized Proof of the Basic Perturbation Lemma. Journal of Automated Reasoning 40(4), 271–292 (2008)

    Article  MATH  Google Scholar 

  3. Capretta, V.: Universal Algebra in Type Theory. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 131–148. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  4. Capretta, V.: Equational Reasoning in Type Theory (preprint)

    Google Scholar 

  5. 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 (LNAI), vol. 4573, pp. 40–54. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. 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)

    Article  MATH  Google Scholar 

  7. Domínguez, C., Rubio, J., Sergeraert, F.: Modeling Inheritance as Coercion in the Kenzo System. Journal of Universal Computer Science 12(12), 1701–1730 (2006)

    Google Scholar 

  8. Dousson, X., Sergeraert, F., Siret, Y.: The Kenzo Program, Institut Fourier, Grenoble (1999), http://www-fourier.ujf-grenoble.fr/sergerar/Kenzo/

  9. Goguen, J., Burstall, R.: Institutions: Abstract Model Theory for Specification and Programming. Journal of the Association for Computing Machinery 39(1), 95–146 (1992)

    MATH  MathSciNet  Google Scholar 

  10. Goguen, J., Malcolm, G.: A Hidden Agenda. Theoretical Computer Science 245, 55–101 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  11. Goguen, J., Malcolm, G., Kemp, T.: A Hidden Herbrand Theorem: Combining the Object, Logic and Functional Paradigms. Journal of Logic and Algebraic Programming 51, 1–41 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  12. Huet, G., Saïbi, A.: Constructive Category Theory. In: Proof, language, and interaction: essays in honour of Robin Milner. Foundations of Computing series, pp. 239–275. MIT Press, Cambridge (2000)

    Google Scholar 

  13. 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)

    Article  MATH  MathSciNet  Google Scholar 

  14. Loeckx, J., Ehrich, H.D., Wolf, M.: Specification of Abstract Data Types. Wiley-Teubner, Chichester (1996)

    MATH  Google Scholar 

  15. LogiCal project. The Coq Proof Assistant (2008), http://coq.inria.fr/

  16. Martin-Löf, P.: Twenty-five years of constructive type theory, Oxford Logic Guides, vol. 36, pp. 127–172 (1998)

    Google Scholar 

  17. Roşu, G.: Hidden Logic. PhD thesis. University of California at San Diego (2000)

    Google Scholar 

  18. Rubio, J.: Locally Effective Objects and Artificial Intelligence. In: Campbell, J.A., Roanes-Lozano, E. (eds.) AISC 2000. LNCS (LNAI), vol. 1930, pp. 223–226. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  19. Rubio, J., Sergeraert, F., Siret, Y.: EAT: Symbolic Software for Effective Homology Computation, Institut Fourier, Grenoble (1997), ftp://ftp-fourier.ujf-grenoble.fr/pub/EAT/

  20. Rubio, J., Sergeraert, F.: Constructive Algebraic Topology. Bulletin Sciences Mathématiques 126, 389–412 (2002)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departamento de Matemáticas y Computación, Universidad de La Rioja, Edificio Vives, Luis de Ulloa s/n, E-26004, Logroño, La Rioja, Spain

    César Domínguez

Authors
  1. César Domínguez
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Serge Autexier John Campbell Julio Rubio Volker Sorge Masakazu Suzuki Freek Wiedijk

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Domínguez, C. (2008). Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds) Intelligent Computer Mathematics. CICM 2008. Lecture Notes in Computer Science(), vol 5144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85110-3_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-85110-3_23

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-85109-7

  • Online ISBN: 978-3-540-85110-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation