Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Formalizing functional analysis structures in dependent type theory

Abstract : This paper discusses the design of a hierarchy of structures which combine linear algebra with concepts related to limits, like topol-ogy 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. This marriage arouses issues of a more general nature, related to the inheritance of poorer structures from richer ones. We present and discuss a solution, coined forgetful inheritance, based on packed classes and unification hints.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download
Contributor : Marie Kerjean <>
Submitted on : Friday, January 31, 2020 - 7:42:34 PM
Last modification on : Thursday, January 7, 2021 - 3:40:10 PM
Long-term archiving on: : Friday, May 1, 2020 - 5:53:15 PM


Files produced by the author(s)


  • HAL Id : hal-02463336, version 1



Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, et al.. Formalizing functional analysis structures in dependent type theory. 2020. ⟨hal-02463336v1⟩



Record views


Files downloads