REPLica: REPL instrumentation for Coq analysis

Talia Ringer, Alex Sanchez-Stern, Dan Grossman, Sorin Lerner

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationCPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020
EditorsJasmin Blanchette, Catalin Hritcu
PublisherAssociation for Computing Machinery, Inc
Pages99-113
Number of pages15
ISBN (Electronic)9781450370974
DOIs
StatePublished - Jan 20 2020
Externally publishedYes
Event9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020 - New Orleans, United States
Duration: Jan 20 2020Jan 21 2020

Conference

Conference9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020
Country/TerritoryUnited States
CityNew Orleans
Period1/20/201/21/20

Keywords

  • Proof engineering
  • Study methodologies
  • User interaction

ASJC Scopus subject areas

  • Computer Science Applications
  • Software

Fingerprint

Dive into the research topics of 'REPLica: REPL instrumentation for Coq analysis'. Together they form a unique fingerprint.

Cite this