Write a Blog >>
Mon 20 Jan 2020 14:43 - 15:05 at Maurepas - Proof engineering and user interaction Chair(s): Yves Bertot

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 Jan

Displayed time zone: Saskatchewan, Central America change

14:00 - 15:05
Proof engineering and user interactionCPP at Maurepas
Chair(s): Yves Bertot INRIA
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 Pennsylvania
DOI 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 Prague
DOI 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 Diego
DOI Pre-print Media Attached