Abstract
In this work we propose a representation of graded algebraic structures and morphisms over them appearing in the field of Homological Algebra in the proof assistants Isabelle and Coq. We provide particular instances of these representations in both systems showing the correctness of the representation. Moreover the adequacy of such representations is illustrated by developing a formal proof of the Trivial Perturbation Lemma in both systems.
This work has been partially supported by the Spanish Government, project MTM2006-06513.
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
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., Domínguez, C.: A Case-Study in Algebraic Manipulation Using Mechanised Reasoning Tools. To appear in International Journal of Computer Mathematics, doi:10.1080/00207160802676604
Coquand, T., Huet, G.: The Calculus of Constructions. Information and Computation 76, 95–120 (1988)
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)
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)
Domínguez, C., Rubio, J., Sergeraert, F.: Modelling Inheritance as Coercion in the Kenzo System. Journal of Universal Computer Science 12(12), 1701–1730 (2006)
The Kenzo Program (1999), http://www-fourier.ujf-grenoble.fr/~sergerar/Kenzo
Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Théry, L.: A Modular Formalisation of Finite Group Theory. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 86–101. Springer, Heidelberg (2007)
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)
Rubio, J., Sergeraert, F.: Constructive Algebraic Topology. Bulletin Sciences Mathématiques 126, 389–412 (2002)
The Coq Proof Assistant (2009), http://coq.inria.fr
The Isabelle Proof Assistant (2009), http://isabelle.in.tum.de
Wiedijk, F. (ed.): The Seventeen Provers of the World, Foreword by Dana S. Scott. LNCS (LNAI), vol. 3600. Springer, Heidelberg (2006)
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
Aransay, J., Domínguez, C. (2009). Modelling Differential Structures in Proof Assistants: The Graded Case. In: Moreno-Díaz, R., Pichler, F., Quesada-Arencibia, A. (eds) Computer Aided Systems Theory - EUROCAST 2009. EUROCAST 2009. Lecture Notes in Computer Science, vol 5717. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04772-5_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-04772-5_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04771-8
Online ISBN: 978-3-642-04772-5
eBook Packages: Computer ScienceComputer Science (R0)