@inproceedings{138c8d9a6e6b4778b691b47b15eea8a8,
title = "REPLica: REPL instrumentation for Coq analysis",
abstract = "Proof engineering tools make it easier to develop and maintain large systems verified using interactive theorem provers. Developing useful proof engineering tools hinges on understanding the development processes of proof engineers. This paper breaks down one barrier to achieving that understanding: remotely collecting granular data on proof developments as they happen. We have built a tool called REPLica that instruments Coq's interaction model in order to collect fine-grained data on proof developments. It is decoupled from the user interface, and designed in a way that generalizes to other interactive theorem provers with similar interaction models. We have used REPLica to collect data over the span of a month from a group of intermediate through expert proof engineers-enough data to reconstruct hundreds of interactive sessions. The data reveals patterns in fixing proofs and in changing programs and specifications useful for the improvement of proof engineering tools. Our experiences conducting this study suggest design considerations both at the level of the study and at the level of the interactive theorem prover that can facilitate future studies of this kind.",
keywords = "Proof engineering, Study methodologies, User interaction",
author = "Talia Ringer and Alex Sanchez-Stern and Dan Grossman and Sorin Lerner",
note = "Funding Information: We thank Enrico Tassi, Ga{\"e}tan Gilbert, Maxime D{\'e}n{\`e}s, Vincent Laporte, and Th{\'e}o Zimmermann for help improving, finalizing, and merging the hooks for distribution in Coq 8.10. We thank Jason Gross for alpha testing REPLica before the study began and reporting bugs. We thank Dimitar Bounov, Martin Kellogg, Chandrakana Nandi, Doug Woos, and Karl Palmskog for help writing and filming the study recruitment video. We thank all who participated in the study or helped distribute promotional materials. We thank the UW PLSE lab, the UCSD Programming Systems group, and the anonymous reviewers for feedback. This material is based upon work supported by the National Science Foundation Graduate Research Fellowship under Grant No. DGE-1256082. Any opinions, findings, and conclusions or recommendations expressedin this material are those of the authors and do not necessarily reflect the views of the National Science Foundation. Publisher Copyright: {\textcopyright} 2020 ACM.; 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020 ; Conference date: 20-01-2020 Through 21-01-2020",
year = "2020",
month = jan,
day = "20",
doi = "10.1145/3372885.3373823",
language = "English (US)",
series = "CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020",
publisher = "Association for Computing Machinery",
pages = "99--113",
editor = "Jasmin Blanchette and Catalin Hritcu",
booktitle = "CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020",
address = "United States",
}