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).


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.


Bibtex entry:

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