Title: Interactive theorem proving with Cambridge LCF
First published: 1985