Tool Support for Proof Engineering

13 years 6 months ago
Tool Support for Proof Engineering
Modern integrated development environments (IDEs) provide programmers with a variety of sophisticated tools for program visualization and manipulation. These tools assist the programmer in understanding legacy code and making coordinated changes across large parts of a program. Similar tools incorporated into an integrated proof environment (IPE) would assist proof developers in understanding and manipulating the increasingly larger proofs that are being developed. In this paper we propose some tools and techniques developed for software engineering that we believe would be equally applicable in proof engineering. Key words: IDE, IPE, proof visualization, program visualization, refactoring, program extraction, Coq, proof dependencies, proof transformations, proof strategies, proof framework, proof reuse, proof explanation
Anne Mulhern, Charles Fischer, Ben Liblit
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Authors Anne Mulhern, Charles Fischer, Ben Liblit
Comments (0)