REPLica: REPL instrumentation for Coq analysis
Talia Ringer, Alex Sanchez-Stern, Dan Grossman, Sorin Lerner · 2020
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.