Packaging Mathematical Structures - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2009

Packaging Mathematical Structures

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (206.87 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00368403 , version 1 (16-03-2009)
inria-00368403 , version 2 (03-07-2009)

Identifiants

  • HAL Id : inria-00368403 , version 2

Citer

François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau. Packaging Mathematical Structures. Theorem Proving in Higher Order Logics, 2009, Munich, Germany. ⟨inria-00368403v2⟩
1134 Consultations
2614 Téléchargements

Partager

Gmail Facebook X LinkedIn More