REPLica: REPL instrumentation for Coq analysis

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

doi:10.1145/3372885.3373823

REPLica: REPL instrumentation for Coq analysis

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

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020
Editors	Jasmin Blanchette, Catalin Hritcu
Publisher	Association for Computing Machinery, Inc
Pages	99-113
Number of pages	15
ISBN (Electronic)	9781450370974
DOIs	https://doi.org/10.1145/3372885.3373823
State	Published - Jan 20 2020
Externally published	Yes
Event	9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020 - New Orleans, United States Duration: Jan 20 2020 → Jan 21 2020

Conference

Conference	9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020
Country/Territory	United States
City	New Orleans
Period	1/20/20 → 1/21/20

Keywords

Proof engineering
Study methodologies
User interaction

ASJC Scopus subject areas

Computer Science Applications
Software

Online availability

10.1145/3372885.3373823

Library availability

Discover UIUC Full Text

Cite this

Ringer, T., Sanchez-Stern, A., Grossman, D., & Lerner, S. (2020). REPLica: REPL instrumentation for Coq analysis. In J. Blanchette, & C. Hritcu (Eds.), CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020 (pp. 99-113). Association for Computing Machinery, Inc. https://doi.org/10.1145/3372885.3373823

REPLica : REPL instrumentation for Coq analysis. / Ringer, Talia; Sanchez-Stern, Alex; Grossman, Dan et al.

CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020. ed. / Jasmin Blanchette; Catalin Hritcu. Association for Computing Machinery, Inc, 2020. p. 99-113.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Ringer, T, Sanchez-Stern, A, Grossman, D & Lerner, S 2020, REPLica: REPL instrumentation for Coq analysis. in J Blanchette & C Hritcu (eds), CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020. Association for Computing Machinery, Inc, pp. 99-113, 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020, New Orleans, United States, 1/20/20. https://doi.org/10.1145/3372885.3373823

@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)",

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",

publisher = "Association for Computing Machinery, Inc",

}

TY - GEN

T1 - REPLica

T2 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020

AU - Ringer, Talia

AU - Sanchez-Stern, Alex

AU - Grossman, Dan

AU - Lerner, Sorin

N1 - Funding Information: We thank Enrico Tassi, Gaëtan Gilbert, Maxime Dénès, Vincent Laporte, and Thé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: © 2020 ACM.

PY - 2020/1/20

Y1 - 2020/1/20

N2 - 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.

AB - 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.

KW - Proof engineering

KW - Study methodologies

KW - User interaction

UR - http://www.scopus.com/inward/record.url?scp=85079469285&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85079469285&partnerID=8YFLogxK

U2 - 10.1145/3372885.3373823

DO - 10.1145/3372885.3373823

M3 - Conference contribution

AN - SCOPUS:85079469285

SP - 99

EP - 113

BT - CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020

A2 - Blanchette, Jasmin

A2 - Hritcu, Catalin

PB - Association for Computing Machinery, Inc

Y2 - 20 January 2020 through 21 January 2020

ER -

REPLica: REPL instrumentation for Coq analysis

Abstract

Conference

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this