Carnegie Mellon University
Towards a Science of Interactive Proof Reading.pdf (221.05 kB)
Download file

Towards a Science of Interactive Proof Reading

Download (221.05 kB)
conference contribution
posted on 2023-03-30, 16:39 authored by Jessica Shi, Benjamin Pierce, Andrew Head

Proof assistants such as Coq are powerful tools for formally verifying the correctness of software. We are interested in the process of reading the proofs produced in this mechanized context, with a goal of building tools to reduce sources of friction and misunderstanding. In this paper, we summarize the early steps we have taken to explore the design space for proof reading support, the results of a pilot study to better understand the proof reading process, and our future plans for this ongoing research.


NSF #1955610, Bringing Python Up to Speed


Usage metrics