John C. Reynolds
Readable Formal Proofs