In Jörg Siekmann (ed), Handbook of the History of Logic, vol. 9: Computational Logic, Elsevier, pp. 135-214 (2014).
@INPROCEEDINGS{harrison-itp, author = "John Harrison and Josef Urban and Freek Wiedijk", title = "History of Interactive Theorem Proving", editor = "J\{"o}rg Siekmann", booktitle = "Handbook of the History of Logic vol. 9 (Computational Logic)", publisher = "Elsevier", year = 2014, pages = "135--214"}