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

Reynald Affeldt; Cyril Cohen; Marie Kerjean; Assia Mahboubi; Damien Rouhling; Kazuhiko Sakaguchi

doi:10.1007/978-3-030-51054-1_1

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

Reynald Affeldt
, Cyril Cohen
, Marie Kerjean
, Assia Mahboubi
, Damien Rouhling
, Kazuhiko Sakaguchi

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

Abstract

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.

Original language	English
Title of host publication	Automated Reasoning
Subtitle of host publication	10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II
Editors	Nicolas Peltier, Viorica Sofronie-Stokkermans
Publisher	Springer
Pages	3-20
Number of pages	18
Volume	2
ISBN (Electronic)	9783030510541
ISBN (Print)	9783030510534
DOIs	https://doi.org/10.1007/978-3-030-51054-1_1
Publication status	Published - 2020
Externally published	Yes
Event	10th International Joint Conference on Automated Reasoning, IJCAR 2020 - Virtual, Online Duration: 1 Jul 2020 → 4 Jul 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12167 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	10th International Joint Conference on Automated Reasoning, IJCAR 2020
City	Virtual, Online
Period	1/07/20 → 4/07/20

Funding

Funders	Funder number
Japan Society for the Promotion of Science	18H03204

Access to Document

10.1007/978-3-030-51054-1_1

Persistent URL (handle)

Persistent link

Cite this

Affeldt, R., Cohen, C., Kerjean, M., Mahboubi, A., Rouhling, D., & Sakaguchi, K. (2020). Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. In N. Peltier, & V. Sofronie-Stokkermans (Eds.), Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II (Vol. 2, pp. 3-20). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12167 LNAI). Springer. https://doi.org/10.1007/978-3-030-51054-1_1

Affeldt, Reynald ; Cohen, Cyril ; Kerjean, Marie et al. / Competing Inheritance Paths in Dependent Type Theory : A Case Study in Functional Analysis. Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II. editor / Nicolas Peltier ; Viorica Sofronie-Stokkermans. Vol. 2 Springer, 2020. pp. 3-20 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{f7419e67da7448ec85dad347b062a24c,

title = "Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis",

abstract = "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.",

author = "Reynald Affeldt and Cyril Cohen and Marie Kerjean and Assia Mahboubi and Damien Rouhling and Kazuhiko Sakaguchi",

year = "2020",

doi = "10.1007/978-3-030-51054-1\_1",

language = "English",

isbn = "9783030510534",

volume = "2",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "3--20",

editor = "Nicolas Peltier and Viorica Sofronie-Stokkermans",

booktitle = "Automated Reasoning",

note = "10th International Joint Conference on Automated Reasoning, IJCAR 2020 ; Conference date: 01-07-2020 Through 04-07-2020",

}

Affeldt, R, Cohen, C, Kerjean, M, Mahboubi, A, Rouhling, D & Sakaguchi, K 2020, Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. in N Peltier & V Sofronie-Stokkermans (eds), Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II. vol. 2, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12167 LNAI, Springer, pp. 3-20, 10th International Joint Conference on Automated Reasoning, IJCAR 2020, Virtual, Online, 1/07/20. https://doi.org/10.1007/978-3-030-51054-1_1

Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. / Affeldt, Reynald; Cohen, Cyril; Kerjean, Marie et al.
Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II. ed. / Nicolas Peltier; Viorica Sofronie-Stokkermans. Vol. 2 Springer, 2020. p. 3-20 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12167 LNAI).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Competing Inheritance Paths in Dependent Type Theory

T2 - 10th International Joint Conference on Automated Reasoning, IJCAR 2020

AU - Affeldt, Reynald

AU - Cohen, Cyril

AU - Kerjean, Marie

AU - Mahboubi, Assia

AU - Rouhling, Damien

AU - Sakaguchi, Kazuhiko

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/85088249913

UR - https://www.scopus.com/pages/publications/85088249913#tab=citedBy

U2 - 10.1007/978-3-030-51054-1_1

DO - 10.1007/978-3-030-51054-1_1

M3 - Conference contribution

SN - 9783030510534

VL - 2

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 3

EP - 20

BT - Automated Reasoning

A2 - Peltier, Nicolas

A2 - Sofronie-Stokkermans, Viorica

PB - Springer

Y2 - 1 July 2020 through 4 July 2020

ER -

Affeldt R, Cohen C, Kerjean M, Mahboubi A, Rouhling D, Sakaguchi K. Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. In Peltier N, Sofronie-Stokkermans V, editors, Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II. Vol. 2. Springer. 2020. p. 3-20. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2020 Jun 24. doi: 10.1007/978-3-030-51054-1_1

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

Abstract

Publication series

Conference

Funding

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this