Tool Support for Proof Engineering
Modern integrated development environments (IDEs) provide programmers with a variety of so-
phisticated 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. Simi-
lar 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.
This is a practice talk for the UITP (User Interfaces for Theorem Provers) workshop at FLoC.
Please come if you can.
-mulhern