Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis

This paper discusses the design of a hierarchy of structures which combine linear algebra with concepts related to limits, like topology 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...

Descripción completa

Detalles Bibliográficos
Autores principales: Affeldt, Reynald, Cohen, Cyril, Kerjean, Marie, Mahboubi, Assia, Rouhling, Damien, Sakaguchi, Kazuhiko
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324078/
http://dx.doi.org/10.1007/978-3-030-51054-1_1
_version_ 1783551875541368832
author Affeldt, Reynald
Cohen, Cyril
Kerjean, Marie
Mahboubi, Assia
Rouhling, Damien
Sakaguchi, Kazuhiko
author_facet Affeldt, Reynald
Cohen, Cyril
Kerjean, Marie
Mahboubi, Assia
Rouhling, Damien
Sakaguchi, Kazuhiko
author_sort Affeldt, Reynald
collection PubMed
description This paper discusses the design of a hierarchy of structures which combine linear algebra with concepts related to limits, like topology 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. Issues of a more general nature related to the inheritance of poorer structures from richer ones arise due to this combination. We present and discuss a solution, coined forgetful inheritance, based on packed classes and unification hints.
format Online
Article
Text
id pubmed-7324078
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73240782020-06-30 Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis Affeldt, Reynald Cohen, Cyril Kerjean, Marie Mahboubi, Assia Rouhling, Damien Sakaguchi, Kazuhiko Automated Reasoning Article This paper discusses the design of a hierarchy of structures which combine linear algebra with concepts related to limits, like topology 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. Issues of a more general nature related to the inheritance of poorer structures from richer ones arise due to this combination. We present and discuss a solution, coined forgetful inheritance, based on packed classes and unification hints. 2020-06-06 /pmc/articles/PMC7324078/ http://dx.doi.org/10.1007/978-3-030-51054-1_1 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Affeldt, Reynald
Cohen, Cyril
Kerjean, Marie
Mahboubi, Assia
Rouhling, Damien
Sakaguchi, Kazuhiko
Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
title Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
title_full Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
title_fullStr Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
title_full_unstemmed Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
title_short Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
title_sort competing inheritance paths in dependent type theory: a case study in functional analysis
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324078/
http://dx.doi.org/10.1007/978-3-030-51054-1_1
work_keys_str_mv AT affeldtreynald competinginheritancepathsindependenttypetheoryacasestudyinfunctionalanalysis
AT cohencyril competinginheritancepathsindependenttypetheoryacasestudyinfunctionalanalysis
AT kerjeanmarie competinginheritancepathsindependenttypetheoryacasestudyinfunctionalanalysis
AT mahboubiassia competinginheritancepathsindependenttypetheoryacasestudyinfunctionalanalysis
AT rouhlingdamien competinginheritancepathsindependenttypetheoryacasestudyinfunctionalanalysis
AT sakaguchikazuhiko competinginheritancepathsindependenttypetheoryacasestudyinfunctionalanalysis

Ejemplares similares