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 - http://www.scopus.com/inward/record.url?scp=85088249913&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-51054-1_1
DO - 10.1007/978-3-030-51054-1_1
M3 - Conference contribution
SN - 9783030510534
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 - 10th International Joint Conference, IJCAR 2020, Proceedings
A2 - Peltier, N.
A2 - Sofronie-Stokkermans, V.
PB - Springer
Y2 - 1 July 2020 through 4 July 2020
ER -