Recycling Proof Patterns in Coq: Case Studies
This work addresses the problem of library reuse in formal verification for theorem prover users, but it is incremental as it builds on existing tools and case studies.
The paper tackled the challenge of reusing proof libraries in Interactive Theorem Provers by evaluating ML4PG, a machine-learning tool that data-mines proof patterns to provide user guidance, resulting in improved accessibility for non-experts and cross-domain applications.
Development of Interactive Theorem Provers has led to the creation of big libraries and varied infrastructures for formal proofs. However, despite (or perhaps due to) their sophistication, the re-use of libraries by non-experts or across domains is a challenge. In this paper, we provide detailed case studies and evaluate the machine-learning tool ML4PG built to interactively data-mine the electronic libraries of proofs, and to provide user guidance on the basis of proof patterns found in the existing libraries.