Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle standard mathematics library, HOL-Ana...


view this post on Zulip Email Gateway (Jul 21 2020 at 20:38):

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: Dec 08 2021 at 09:20 UTC