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.
Type de document :
Communication dans un congrès
CICM 2015, Jul 2015, Washington DC, United States. Lecture Notes in Computer Science, 2015, Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. 〈10.1007/978-3-319-20615-8_1〉
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01212594
Contributeur : Jasmin Christian Blanchette <>
Soumis le : mercredi 7 octobre 2015 - 10:09:19
Dernière modification le : lundi 20 novembre 2017 - 15:14:02
Document(s) archivé(s) le : vendredi 8 janvier 2016 - 10:16:11

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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. Lecture Notes in Computer Science, 2015, Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. 〈10.1007/978-3-319-20615-8_1〉. 〈hal-01212594〉

Partager

Métriques

Consultations de la notice

272

Téléchargements de fichiers

61