=Paper=
{{Paper
|id=Vol-2634/LML-preface
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-2634/LML-preface.pdf
|volume=Vol-2634
}}
==None==
<pdf width="1500px">https://ceur-ws.org/Vol-2634/LML-preface.pdf</pdf>
<pre>
                   Large Mathematics Libraries (LML 2019)




   Large formal and semiformal mathematics libraries are needed to support mathematics research, mathematics
education, rigorous software development, and formal proof development. This workshop explores methods
for designing, constructing, and maintaining large mathematics libraries as well as for finding, comparing, and
applying the knowledge residing in these libraries. The key topics of interest are:
  • Methods for sharing knowledge between libraries.
  • Modular techniques for organizing the knowledge within libraries.

  • The translation of libraries to different languages and logics.
  • The construction of new libraries by integrating existing libraries.
  • Tools for exploring the contents of large libraries.
   The highlights of workshop are two invited talks, the first “Isabelle technology for the Archive of Formal Proofs
with application to MMT” by Makarius Wenzel and the second “Attempts at Skinning the Elephant” by Claudio
Sacerdoti Coen on applications of CICM technology to the Coq library.




Copyright © by the paper’s authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
In: C. Kaliszyk, E. Brady, J. Davenport, W.M. Farmer, A. Kohlhase, M. Kohlhase, D. Müller, K. Pąk, and C. Sacerdoti Coen (eds.):
Joint Proceedings of the FMM and LML Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent
Computer Mathematics 2019 co-located with the 12th Conference on Intelligent Computer Mathematics (CICM 2019), Prague,
Czech Republic, July 8–12, 2019, published at http://ceur-ws.org

</pre>