Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis.
IJCAR (2)(2020)
摘要
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.
更多查看译文
关键词
Formalization of mathematics, Dependent type theory, Packed classes, Coq
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络