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 metadatas

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-01212594
Contributor : Jasmin Blanchette <>
Submitted on : Wednesday, October 7, 2015 - 10:09:19 AM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
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

Record views

455

Files downloads

276