Data type proofs using Edinburgh LCF - Monahan, Brian Quentin (The University of Edinburgh, 1984)