# Proof repair across type equivalences

@article{Ringer2021ProofRA, title={Proof repair across type equivalences}, author={Talia Ringer and Randair Porter and Nathaniel Yazdani and J. Leo and Dan Grossman}, journal={Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation}, year={2021} }

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 transformation with a decompiler from proof terms to suggested tactic scripts. The proof term transformation implements transport across equivalences in a way that removes references to the old version of the changed type and does not rely on axioms beyond those Coq assumes. We have implemented this approach in Pumpkin Pi… Expand

#### References

SHOWING 1-10 OF 69 REFERENCES

Adapting proof automation to adapt proofs

- Computer Science
- CPP
- 2018

This work identifies and implements five core components that are key to searching for a patch that can be applied to other specifications and proofs that need to change in analogous ways and builds a patch finding procedure from these components. Expand

REPLica: REPL instrumentation for Coq analysis

- Computer Science
- CPP
- 2020

A tool is built that instruments Coq’s interaction model in order to collect fine-grained data on proof developments as they happen, and is decoupled from the user interface, and designed in a way that generalizes to other interactive theorem provers with similar interaction models. Expand

Theorem Reuse by Proof Term Transformation

- Computer Science, Mathematics
- TPHOLs
- 2004

This paper proposes an approach where theorems are generalised by abstracting their proofs from the original setting, based on a representation of proofs as logical framework proof terms, using the theorem prover Isabelle. Expand

Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant

- Computer Science
- 2013

This book provides an introduction to the Coq software for writing and checking mathematical proofs, with a practical engineering focus throughout, emphasizing techniques that will help users to build, understand, and maintain large Coq developments and minimize the cost of code change over time. Expand

Generalization and Reuse of Tactic Proofs

- Computer Science
- LPAR
- 1994

A prototype of a generic interactive theorem-proving system that supports the construction and manipulation of tactic proofs containing metavariables is described, with the emphasis on proof reuse. Expand

Challenges and Experiences in Managing Large-Scale Proofs

- Computer Science
- AISC/MKM/Calculemus
- 2012

The main challenges in large-scale proofs are identified, possible solutions are proposed, and the Levity tool, which was developed to automatically move lemmas to appropriate theories, is discussed, as an example of the kind of tool required by such proofs. Expand

TacTok: semantics-aware proof synthesis

- Computer Science
- Proc. ACM Program. Lang.
- 2020

TacTok is presented, the first technique that attempts to fully automate proof script synthesis by modeling proof scripts using both the partial proof script written thus far and the semantics of the proof state, and evidence that metaheuristic search is a promising direction forProof script synthesis is provided. Expand

QED at Large: A Survey of Engineering of Formally Verified Software

- Computer Science
- Found. Trends Program. Lang.
- 2019

A survey of the literature presents a holistic understanding of proof engineering for program correctness, covering impact in practice, foundations, proof automation, proof organization, and practical proof development. Expand

Refinements for Free!

- Computer Science
- CPP
- 2013

This work introduces a framework where correctness is established in a proof-oriented context and automatically transported to computation-oriented data structures and the rich formalism of the Coq proof assistant enables this to be developed within Coq, without having to maintain an external tool. Expand

CoqPIE: An IDE Aimed at Improving Proof Development Productivity - (Rough Diamond)

- Engineering, Computer Science
- ITP
- 2016

A new development environment for Coq which delivers editing functionality centered around common prover usage workflow not found in existing tools, and includes tools to carry out complex editing functions such as lemma extraction and replay. Expand