HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Packaging Mathematical Structures

François Garillot 1, * Georges Gonthier 2, * Assia Mahboubi 3, * Laurence Rideau 4, *
* Corresponding author
3 TYPICAL - Types, Logic and computing
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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.
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download

Contributor : Assia Mahboubi Connect in order to contact the contributor
Submitted on : Friday, July 3, 2009 - 7:23:39 PM
Last modification on : Thursday, January 20, 2022 - 5:30:47 PM
Long-term archiving on: : Saturday, November 26, 2016 - 9:48:12 AM


Files produced by the author(s)


  • HAL Id : inria-00368403, version 2



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



Record views


Files downloads