inria-00368403, version 2

Voir la fiche détaillée

BibTeX  EndNote  TEI  RefWorks %% inria-00368403, version 2 %% http://hal.inria.fr/inria-00368403/en/ @inproceedings{GARILLOT:2009:INRIA-00368403:2, title = { {P}ackaging {M}athematical {S}tructures}, author = {{G}arillot, {F}ran{\c{c}}ois and {G}onthier, {G}eorges and {M}ahboubi, {A}ssia and {R}ideau, {L}aurence}, abstract = {{T}his paper proposes generic design patterns to define and combine algebraic structures, using dependent records, coercions and type inference, inside the {C}oq system. {T}his alternative to telescopes in particular allows multiple inheritance, maximal sharing of notations and theories, and automated structure inference. {O}ur 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. {I}nterfaces for the structures enjoy the handiness of a classical setting, without requiring any axiom. {F}inally, 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.}, keywords = {{F}ormalization of {A}lgebra, {C}oercive subtyping, {T}ype inference, {C}oq, {SSR}eflect}, language = {{A}nglais}, affiliation = {{M}icrosoft {R}esearch {I}nria - {MRI} - {INRIA} - {M}icrosoft - {M}icrosoft {R}esearch {C}ambridge - {M}icrosoft - {M}icrosoft {R}esearch - {T}ypi{C}al - {INRIA} {S}aclay - {I}le de {F}rance - {INRIA} - {CNRS} : {UMR} - {P}olytechnique - {X} - {MARELLE} - {INRIA} {S}ophia {A}ntipolis - {INRIA} }, booktitle = {{T}heorem {P}roving in {H}igher {O}rder {L}ogics }, publisher = {{S}pringer }, address = {{M}unich {A}llemagne }, volume = {5674 }, editor = {{T}obias {N}ipkow and {C}hristian {U}rban }, series = {{L}ecture {N}otes in {C}omputer {S}cience }, note = {{G}.: {M}athematics of {C}omputing/{G}.4: {MATHEMATICAL} {SOFTWARE}, {I}.: {C}omputing {M}ethodologies/{I}.1: {SYMBOLIC} {AND} {ALGEBRAIC} {MANIPULATION}/{I}.1.0: {G}eneral }, audience = {internationale }, year = {2009}, URL = {http://hal.inria.fr/inria-00368403/en/}, URL = {http://hal.inria.fr/inria-00368403/PDF/main.pdf}, } %F inria-00368403, version 2 %0 Conference Proceedings %U http://hal.inria.fr/inria-00368403/en/ %2 INFO:INFO_LO;MATH:MATH_GM %T Packaging Mathematical Structures %A Garillot, François %A Gonthier, Georges %A Mahboubi, Assia %A Rideau, Laurence %A Garillot, F. %A Gonthier, G. %A Mahboubi, A. %A Rideau, L. %A Garillot F. et al %+ Microsoft Research Inria - MRI - INRIA - Microsoft - Microsoft Research Cambridge - Microsoft - Microsoft Research - TypiCal - INRIA Saclay - Ile de France - INRIA - CNRS : UMR - Polytechnique - X - MARELLE - INRIA Sophia Antipolis - INRIA %X 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. %2 G.: Mathematics of Computing/G.4: MATHEMATICAL SOFTWARE, I.: Computing Methodologies/I.1: SYMBOLIC AND ALGEBRAIC MANIPULATION/I.1.0: General %G Anglais %8 2009 %2 internationale %B Theorem Proving in Higher Order Logics %2 Munich %2 Allemagne %8 2009 %E Tobias Nipkow and Christian Urban %I Springer %V 5674 %N Lecture Notes in Computer Science %K Formalization of Algebra, Coercive subtyping, Type inference, Coq, SSReflect <?xml version="1.0" encoding="UTF-8"?> <listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML"> <listBibl type="inproceedings"><head>Communications avec acte</head> <biblStruct type="inproceedings" xml:id="inria-00368403"><analytic> <author><persName><forename>François</forename><surname>Garillot</surname></persName> <affiliation> <orgName type="laboratory">MRI</orgName> <orgName type="team">Microsoft Research Inria</orgName> <country>FR</country> <orgName type="institution">INRIA</orgName> <orgName type="institution">Microsoft</orgName> </affiliation> </author> <author><persName><forename>Georges</forename><surname>Gonthier</surname></persName> <affiliation> <orgName type="laboratory">Microsoft</orgName> <orgName type="team">Microsoft Research Cambridge</orgName> <country>GB</country> <orgName type="institution">Microsoft Research</orgName> </affiliation> </author> <author><persName><forename>Assia</forename><surname>Mahboubi</surname></persName> <affiliation> <orgName type="laboratory">INRIA Saclay - Ile de France</orgName> <orgName type="team">TypiCal</orgName> <country>FR</country> <orgName type="institution">INRIA</orgName> <orgName type="institution">CNRS : UMR</orgName> <orgName type="institution">Polytechnique - X</orgName> </affiliation> </author> <author><persName><forename>Laurence</forename><surname>Rideau</surname></persName> <affiliation> <orgName type="laboratory">INRIA Sophia Antipolis</orgName> <orgName type="team">MARELLE</orgName> <country>FR</country> <orgName type="institution">INRIA</orgName> </affiliation> </author> <title type="main" level="a">Packaging Mathematical Structures</title></analytic><monogr><meeting>Theorem Proving in Higher Order Logics</meeting><imprint><publisher>Springer</publisher><pubPlace><settlement>Munich</settlement><country>Allemagne</country></pubPlace><biblScope type="publicationDate">2009</biblScope><biblScope type="vol">5674</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00368403/en/</idno><idno type="HALFile">http://hal.inria.fr/inria-00368403/PDF/main.pdf</idno></biblStruct> </listBibl> </listBibl>

Packaging Mathematical Structures François Garillot (  Auteur à contacter de préférence , ) 1, Georges Gonthier (  Auteur à contacter de préférence , ) 2, Assia Mahboubi (  Auteur à contacter de préférence , ) 3, Laurence Rideau (  Auteur à contacter de préférence , ) 4 (2009)

Accès au texte intégral PDF

Theorem Proving in Higher Order Logics 5674 (2009)

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.

1 :	Microsoft Research Inria (MRI)
	INRIA – Microsoft
2 :	Microsoft Research Cambridge (Microsoft)
	Microsoft Research
3 :	TypiCal (INRIA Saclay - Ile de France)
	INRIA – CNRS : UMR – Polytechnique - X
4 :	MARELLE (INRIA Sophia Antipolis)
	INRIA

Domaine

:

Informatique/Logique en informatique Mathématiques/Mathématiques générales

Mots-clés : Formalization of Algebra – Coercive subtyping – Type inference – Coq – SSReflect

Versions disponibles :

v1 (16-03-2009)

v2 (03-07-2009)

inria-00368403, version 2

http://hal.inria.fr/inria-00368403/fr/

oai:hal.inria.fr:inria-00368403_v2

Contributeur : Assia Mahboubi <>

Soumis le : Vendredi 3 Juillet 2009, 19:23:39

Dernière modification le : Jeudi 9 Juillet 2009, 13:17:34