Tool Support for Proof EngineeringTool Support for Proof EngineeringThis research was conducted by Anne Mulhern, Charles Fischer, and Ben Liblit. The paper has been published in the 2006 Workshop on User Interfaces for Theorem Provers (UITP 2006).
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.
The full paper is available as a single PDF document. A suggested BibTeX citation record is also available.