Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
复制标题
DOI：
10.1007/978-3-030-51054-1_1
复制
发表时间：
2020-06-06
期刊：
影响因子：
--
通讯作者：
Sakaguchi K
中科院分区：
文献类型：
--
作者：
Affeldt R;Cohen C;Kerjean M;Mahboubi A;Rouhling D;Sakaguchi K
本文讨论了将线性代数与相依型理论中与极限相关的概念(如拓扑和范数)相结合的层次结构的设计。这个层次结构是一个新的形式化经典分析库的骨干，用于CoQ证明助手。它扩展了面向代数的数学组件库，增加了分析主题。由于这种组合，出现了与较差的结构从较丰富的结构继承有关的更一般性质的问题。我们提出并讨论了一种解决方案，基于打包的类和统一提示，创造了健忘继承。
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.
登录
查看更多内容
影响因子：
0.8
作者：
Boldo, Sylvie;Lelay, Catherine;Melquiond, Guillaume
通讯作者：
Melquiond, Guillaume
影响因子：
0.6
作者：
Cohen, Cyril;Mahboubi, Assia
通讯作者：
Mahboubi, Assia
影响因子：
0.5
作者：
Spitters, Bas;Van der Weegen, Eelis
通讯作者：
Van der Weegen, Eelis
DOI：
10.1007/978-3-030-51054-1_8
发表时间：
2020-06-06
期刊：
Automated Reasoning
影响因子：
--
作者：
Sakaguchi K
通讯作者：
Sakaguchi K
影响因子：
1
作者：
DEBRUIJN, NG
通讯作者：
DEBRUIJN, NG