Towards Mining Robust Coq Proof Patterns

This conference talk from CoqPL 2025 explores an innovative approach to reducing human effort in maintaining Coq formal proof scripts through mining robust proof patterns. Presented by researchers Cezary Kaliszyk, Xuan-Bach D. Le, and Christine Rizkallah from the University of Melbourne, the 19-minute presentation details their plan to adapt software engineering program repair methodologies for proof repair. Learn about their proposed mining approach using a recently published Coq dataset and how established software maintenance techniques could benefit proof maintenance. The speakers specifically sought feedback from the Coq community on their planned methodology during this ACM SIGPLAN-sponsored workshop held on January 25, 2025.