Porting Coq Scripts to the Mathematical Components Library Version 2
In: https://hal.science/hal-04225130 ; Inria Sophia Antipolis - Méditerranée, Université Côte d'Azur; National Institute of Advanced Industrial Science and Technology (AIST), Japan; ONERA / DTIS, 2023
Online
report
Zugriff:
The Mathematical Components library (hereafter, MathComp) provides, among others, a number of mathematical structures organized as hierarchies. Hierarchy Builder (hereafter, HB) is an extension of the Coq proof assistant to ease the development of hierarchies of structures. MathComp 2 is the result of the port of MathComp to HB. This document is a technical report whose goal is to explain how to port MathComp developments to MathComp 2. It has been written by the participants of the MathComp Documentation Sprint that happened from 2023-05-03 to 2023-05-10.
| Titel: |
Porting Coq Scripts to the Mathematical Components Library Version 2
|
|---|---|
| Autor/in / Beteiligte Person: | Affeldt, Reynald ; Bertot, Yves ; Cohen, Cyril ; Roux, Pierre ; Sakaguchi, Kazuhiko ; Tassi, Enrico ; National Institute of Advanced Industrial Science and Technology (AIST) ; Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) ; DTIS, ONERA, Université de Toulouse Toulouse ; ONERA-PRES Université de Toulouse ; Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE) ; Inria Rennes – Bretagne Atlantique ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique) ; Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-NANTES UNIVERSITÉ - École Centrale de Nantes (Nantes Univ - ECN) ; Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes université - UFR des Sciences et des Techniques (Nantes univ - UFR ST) ; Nantes Université - pôle Sciences et technologie ; Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes Université - pôle Sciences et technologie ; Nantes Université (Nantes Univ)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique) ; Nantes Université (Nantes Univ) ; Inria Sophia Antipolis - Méditerranée, Université Côte d'Azur ; National Institute of Advanced Industrial Science and Technology (AIST), Japan ; ONERA / DTIS, Université de Toulouse, France |
| Link: | |
| Zeitschrift: | https://hal.science/hal-04225130 ; Inria Sophia Antipolis - Méditerranée, Université Côte d'Azur; National Institute of Advanced Industrial Science and Technology (AIST), Japan; ONERA / DTIS, 2023 |
| Veröffentlichung: | HAL CCSD, 2023 |
| Medientyp: | report |
| Schlagwort: |
|
| Sonstiges: |
|