ECOOP 2025
Mon 30 June - Fri 4 July 2025 Bergen, Norway
Wed 2 Jul 2025 16:15 - 16:36 at Auditorium M003 - W3 Chair(s): Carla Ferreira

Proof engineering in Coq is a labor-intensive process, and as proof developments grow in size, redundancy and maintainability become significant challenges. One such redundancy is \textit{goal cloning}, i.e., proving $\alpha$-equivalent goals multiple times, leading to wasted effort and bloated proof scripts. In this paper, we introduce clone-finder, a novel technique for detecting goal clones in Coq proofs. By leveraging the formal notion of $\alpha$-equivalence for Gallina terms, clone-finder systematically identifies duplicated proof goals across large Coq codebases. We evaluate clone-finder on 40 real-world Coq projects from the CoqGym dataset. Our results reveal that each project contains an average of 16.9 instances of goal clone. We observed that the clones can be categorized as either \textit{exact goal duplication}, \textit{generalization}, or \textit{$\alpha$-equivalent goals with different proofs}, each signifying varying levels duplicate effort. Our findings highlight significant untapped potential for proof reuse in Coq-based formal verification projects, paving the way for future improvements in automated proof engineering.

Wed 2 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:15 - 17:39
W3Technical Papers at Auditorium M003
Chair(s): Carla Ferreira NOVA University Lisbon
16:15
21m
Talk
Automatic Goal Clone Detection in Rocq
Technical Papers
Ali Ghanbari Auburn University
16:36
21m
Talk
Contract Usage and Evolution in Android Mobile Applications
Technical Papers
David R. Ferreira Faculty of Engineering, University of Porto, Alexandra Mendes Faculty of Engineering, University of Porto & INESC TEC, João F. Ferreira INESC-ID and IST, University of Lisbon, Carolina Carreira Carnegie Mellon University, IST University of Lisbon, INESC-ID
16:57
21m
Talk
Chain of Grounded Objectives: Concise Goal-oriented Prompting for Code Generation
Technical Papers
Sangyeop Yeo ETRI (Electronics and Telecommunications Research Institute), seung-won hwang Seoul National University, Yu-Seung Ma Electronics and Telecommunications Research Institute
17:18
21m
Talk
Contract Systems Need Domain-Specific Notations
Technical Papers
Cameron Moy Northeastern University, Ryan Jung PLT @ Northeastern University, Matthias Felleisen Northeastern University