49 citations · 102 across the 7 of their papers we have counts for
Showing 2020Show all
2 papers · 1 filter
cs.PL2020★ 20 cited
Proof Repair across Type Equivalences
Talia Ringer, RanDair Porter, Nathaniel Yazdani +2
We describe a new approach to automatically repairing broken proofs in the Coq proof assistant in response to changes in types. Our approach combines a configurable proof term tran…
cs.LO2020★ 49 cited
QED at Large: A Survey of Engineering of Formally Verified Software
Talia Ringer, Karl Palmskog, Ilya Sergey +2
Development of formal proofs of correctness of programs can increase actual and perceived reliability and facilitate better understanding of program specifications and their underl…