Harrison, John,
Urban, Josef and
Wiedijk, Freek. 2014.
“Interactive Theorem Proving.” in
Handbook of the History of Logic. Volume 9: Computational Logic, edited by Jörg H.
Siekmann and Dov M.
Gabbay, pp. 135–214. Amsterdam: Elsevier Science Publishers B.V.