Packaging Mathematical Structures
In: Lecture Notes in Computer Science ISBN: 9783642033582 TPHOLs Theorem Proving in Higher Order Logics Theorem Proving in Higher Order Logics, 2009, Munich, Germany; (2009)
Online
unknown
Zugriff:
International audience; 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.
| Titel: |
Packaging Mathematical Structures
|
|---|---|
| Autor/in / Beteiligte Person: | Gonthier, Georges ; Rideau, Laurence ; Mahboubi, Assia ; Garillot, François ; Microsoft Research - Inria Joint Centre (MSR - INRIA) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Microsoft Research Laboratory Cambridge-Microsoft Corporation [Redmond, Wash.] ; Microsoft Research [Cambridge] (Microsoft) ; Research, Microsoft ; Types, Logic and computing (TYPICAL) ; Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX) ; École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) ; Mathematical, Reasoning and Software (MARELLE) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Tobias Nipkow and Christian Urban ; Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France |
| Link: | |
| Quelle: | Lecture Notes in Computer Science ISBN: 9783642033582 TPHOLs Theorem Proving in Higher Order Logics Theorem Proving in Higher Order Logics, 2009, Munich, Germany; (2009) |
| Veröffentlichung: | Springer Berlin Heidelberg, 2009 |
| Medientyp: | unknown |
| ISBN: | 978-3-642-03358-2 (print) |
| DOI: | 10.1007/978-3-642-03359-9_23 |
| Schlagwort: |
|
| Sonstiges: |
|