Skip to Main content Skip to Navigation
Conference papers

Mining the Archive of Formal Proofs

Abstract : The Archive of Formal Proofs is a vast collection of computer-checked proofs developed using the proof assistant Isabelle. We perform an in-depth analysis of the archive, looking at various properties of the proof developments, including size, dependencies, and proof style. This gives some insights into the nature of formal proofs.
Document type :
Conference papers
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-01212594
Contributor : Jasmin Blanchette Connect in order to contact the contributor
Submitted on : Wednesday, October 7, 2015 - 10:09:19 AM
Last modification on : Thursday, January 6, 2022 - 11:38:04 AM
Long-term archiving on: : Friday, January 8, 2016 - 10:16:11 AM

File

paper.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, Tobias Nipkow. Mining the Archive of Formal Proofs. CICM 2015, Jul 2015, Washington DC, United States. ⟨10.1007/978-3-319-20615-8_1⟩. ⟨hal-01212594⟩

Share

Metrics

Les métriques sont temporairement indisponibles