Email Gateway (Aug 23 2022 at 09:22): Email Gateway (Aug 23 2022 at 09:22):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
I am looking for the original conference proceedings/journal articles or
technical reports that describe the following libraries that are available
from the main distribution of Isabelle/HOL:
- Standard mathematics library that is available from Main/Complex_Main
- HOL-Algebra
- HOL-Analysis
For the standard mathematics library, I am aware of [1]. Is this the most
appropriate reference? For HOL-Algebra, I was not able to find any relevant
publications. It seems that [2] is relevant for HOL-Analysis, but I am not
certain if this is the only article and/or the most relevant one, as it
seems to cover only one part of the library. Any help/advice on how to
reference these libraries in the most appropriate manner would be highly
appreciated.
Kind Regards,
Mikhail Chekhov
[1] Hölzl J, Immler F, Huffman B. Type Classes and Filters for Mathematical
Analysis in Isabelle/HOL. In: Blazy S, Paulin-Mohring C, Pichardie D,
editors. Interactive Theorem Proving. Berlin, Heidelberg: Springer Berlin
Heidelberg; 2013. p. 279–94. (Lecture Notes in Computer Science; vol.
7998).
[2] Hölzl J, Heller A. Three Chapters of Measure Theory in Isabelle/HOL.
In: van Eekelen M, Geuvers H, Schmaltz J, Wiedijk F, editors. Interactive
Theorem Proving. Berlin, Heidelberg: Springer Berlin Heidelberg; 2011. p.
135–51. (Lecture Notes in Computer Science; vol. 6898).
Last updated: Nov 21 2024 at 12:39 UTC