Workshop on Proof Enginnering: Constructing, Maintaining and Understanding Large Proofs

The past decade has seen some very large formal proofs produced, with some impressive milestone achievements. However, the tools for developing formal proofs and maintaining and documenting them are still in their infancy, compared with the methodology and tools available for software engineering. Developing formal proof is often an activity conducted or directed by a strong individual, rather than routinely being a collaborative activity.

The aim of this workshop is to bring together researchers interested in the new field of Proof Engineering, defined to mean the construction, maintenance, documentation and presentation of large formal proof developments. Proof Engineering will combine the best of software engineering with the best of computer-checked formal proof: software engineering provides the techniques to develop large, structured and well-specified repositories of computer code; proof checking provides the mechanisms to provide a complete semantics and formal correctness as an absolute quality criterion; and mathematical knowledge management provides the foundations to handle such large bodies of proof text.

Organizers

• David Aspinall School of Informatics, University of Edinburgh, Scotland
• Christoph Lüth, DFKI Bremen & University of Bremen, Germany