We present an authoring system for formal proof which addresses the concerns of efficiently producing formal proof developments together with human-readable documentation. To start, we consider a central document format which, in the tradition of literate programming, allows one to extract either a formal proof script or a human-readable rendering; the two may have differing structure and detail levels, but are developed together in a synchronised way. On top of this, we introduce ways for assisting the production of the central document, by allowing tools to contribute backflow to update and extend the document automatically. Our authoring system extends the new PG Kit architecture for Proof General, which brings the extra advantage that it fits into a uniform interface that is generic across different theorem proving systems.David Aspinall, Christoph Lüth and Burkhart Wolff.
Click here to return to my papers page.
David R. Aspinall, email david.aspinall@ed.ac.uk.