REPLICA: REPL Instrumentation for Coq Analysis
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.
Mon 20 JanDisplayed time zone: Saskatchewan, Central America change
14:00 - 15:05
|An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction|
Yannick Zakowski University of Pennsylvania, Paul He University of Pennsylvania, Chung-Kil Hur Seoul National University, Steve Zdancewic University of PennsylvaniaDOI Pre-print Media Attached File Attached
|Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar|
Qingxiang Wang University of Innsbruck, Chad Brown Czech Technical University in Prague, Cezary Kaliszyk University of Innsbruck, Josef Urban Czech Technical University in PragueDOI Pre-print
|REPLICA: REPL Instrumentation for Coq Analysis|
Talia Ringer University of Washington, Alex Sanchez-Stern University of California, San Diego, Dan Grossman University of Washington, Sorin Lerner University of California, San DiegoDOI Pre-print Media Attached