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
Liste complète des métadonnées

Cited literature [29 references]  Display  Hide  Download

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

423

Files downloads

173