skip to content
 

Mining the Archive of Formal Proofs

Presented by: 
Tobias Nipkow Technischen Universität München
Date: 
Thursday 13th July 2017 - 10:00 to 11:00
Venue: 
INI Seminar Room 1
Abstract: 

 

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

 

Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons