Packaging Mathematical Structures

François Garillot 1, * Georges Gonthier 2, * Assia Mahboubi 3, * Laurence Rideau 4, *
* Auteur correspondant
3 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR
4 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : This paper proposes generic design patterns to define and combine algebraic structures, using dependent records, coercions and type inference, inside the Coq system. This alternative to telescopes in particular allows multiple inheritance, maximal sharing of notations and theories, and automated structure inference. Our methodology is robust enough to support a hierarchy comprising a broad variety of algebraic structures, from types with a choice operator to algebraically closed fields. Interfaces for the structures enjoy the handiness of a classical setting, without requiring any axiom. Finally, we show how externally extensible some of these instances are by discussing a lemma seminal in defining the discrete logarithm, and a matrix decomposition problem.
Type de document :
Communication dans un congrès
Tobias Nipkow and Christian Urban. Theorem Proving in Higher Order Logics, 2009, Munich, Germany. Springer, 5674, 2009, Lecture Notes in Computer Science
Liste complète des métadonnées


https://hal.inria.fr/inria-00368403
Contributeur : Assia Mahboubi <>
Soumis le : vendredi 3 juillet 2009 - 19:23:39
Dernière modification le : jeudi 9 février 2017 - 15:10:04
Document(s) archivé(s) le : samedi 26 novembre 2016 - 09:48:12

Fichier

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

Identifiants

  • HAL Id : inria-00368403, version 2

Collections

Citation

François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau. Packaging Mathematical Structures. Tobias Nipkow and Christian Urban. Theorem Proving in Higher Order Logics, 2009, Munich, Germany. Springer, 5674, 2009, Lecture Notes in Computer Science. <inria-00368403v2>

Partager

Métriques

Consultations de
la notice

988

Téléchargements du document

458