Canonical Big Operators

Abstract : In this paper, we present an approach to describe uniformly iterated “big” operations and to provide lemmas that encapsulate all the commonly used reasoning steps on these constructs. We show that these iterated operations can be handled generically using the syntactic notation and canonical structure facilities provided by the Coq system. We then show how these canonical big operations played a crucial enabling role in the study of various parts of linear algebra and multi-dimensional real analysis, as illustrated by the formal proofs of the properties of determinants, of the Cayley-Hamilton theorem and of Kantorovitch's theorem.
Type de document :
Communication dans un congrès
Theorem Proving in Higher Order Logics, Aug 2008, Montreal, Canada. 5170/2008, 2008, LNCS. <10.1007/978-3-540-71067-7>
Liste complète des métadonnées


https://hal.inria.fr/inria-00331193
Contributeur : Ioana Pasca <>
Soumis le : mercredi 15 octobre 2008 - 16:04:12
Dernière modification le : lundi 5 octobre 2015 - 16:59:45
Document(s) archivé(s) le : mardi 9 octobre 2012 - 13:50:08

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca. Canonical Big Operators. Theorem Proving in Higher Order Logics, Aug 2008, Montreal, Canada. 5170/2008, 2008, LNCS. <10.1007/978-3-540-71067-7>. <inria-00331193>

Partager

Métriques

Consultations de
la notice

648

Téléchargements du document

348