| Autor: |
Affeldt, Reynald, Cohen, Cyril, Kerjean, Marie, Mahboubi, Assia, Rouhling, Damien, Sakaguchi, Kazuhiko |
| Přispěvatelé: |
National Institute of Advanced Industrial Science and Technology (AIST), Mathematical, Reasoning and Software (MARELLE), 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), Laboratoire des Sciences du Numérique de Nantes (LS2N), Université de Nantes - Faculté des Sciences et des Techniques, Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Symbolic Special Functions : Fast and Certified (SPECFUN), Inria Saclay - Ile de France, École normale supérieure - Lyon (ENS Lyon), University of Tsukuba |
| Jazyk: |
angličtina |
| Rok vydání: |
2020 |
| Předmět: |
|
| Popis: |
This paper discusses the design of a hierarchy of structures which combine linear algebra with concepts related to limits, like topol-ogy and norms, in dependent type theory. This hierarchy is the backbone of a new library of formalized classical analysis, for the Coq proof assistant. It extends the Mathematical Components library, geared towards algebra, with topics in analysis. This marriage arouses issues of a more general nature, related to the inheritance of poorer structures from richer ones. We present and discuss a solution, coined forgetful inheritance, based on packed classes and unification hints. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
