History of Interactive Theorem Proving

John Harrison, Josef Urban and Freek Wiedijk.

In Jörg Siekmann (ed), Handbook of the History of Logic, vol. 9: Computational Logic, Elsevier, pp. 135-214 (2014).

Abstract:

This book chapter gives a historical overview of the whole field of interactive theorem proving, with particular emphasis on the systems that introduced some of the key ideas that are still important.

PDF

Bibtex entry:

@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"}