Simons M., Biersack M., Raschke R. (1996) Literate and Structured Presentation of Formal Proofs. In: Olderog E.-R. (ed.) IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET'94)' (pp.61-81). North-Holland.
© North-Holland

Abstract The paper focusses on the literate and structured presentation of formal proofs. The approach presented is influenced by Leslie Lamport's ideas on how to write proofs, by Donald Knuth's paradigm of literate programming, and by the concepts of calculational reasoning. The approach is illustrated with the proofs of two mathematical theorems--the Knaster-Tarski fixpoint theorem and the Schröder-Bernstein theorem--formalized in Deva. We discuss to what degree our aims have been achieved and what work remains to be done. The paper was written using the DevaWEB-system, and the Deva formalization was checked by an implementation of Deva.