REPLica: REPL Instrumentation for Coq Analysis
summary
REPLica instruments the Coq read‑eval‑print loop with a client‑server plugin and records every interaction (timestamps, REPL inputs and responses) across UIs; the implementation works on Coq 8.10 with backports to 8.8/8.9 and is on GitHub. A month‑long study of eight users yields a public dataset and analyses: 75% of proof fixes are made by changing code or specs elsewhere (75%), one benchmark shows one inductive‑type refactor spanning five sessions, three weeks and 63 edits, and the paper lists 11 benchmarks plus three infrastructure wishes.
AI-written summary · about
chapters (5)
related talks
15mA Principled Approach to REPL Interpreters
16mUntangling Mechanized Proofs
46mSession with the Coq Development Team
31mA Coq Library of Undecidable Problems
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
23mVellvm: Formalizing the Informal
42mMetaCoq as a tool to prevent future unsoundness in Coq
15mSulfur: Substitution Generation using a Logical Framework