skip to content

Mining the Archive of Formal Proofs

Presented by: 
Tobias Nipkow
Thursday 13th July 2017 - 10:00 to 11:00
INI Seminar Room 1
Co-authors: Jasmin Christian Blanchette (Vrije Universiteit Amsterdam), Maximilian Haslbeck (Technical University Munich), Daniel Matichuk (Data61) 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.Related Links - Paper - Archive of Formal Proofs
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons