@incollection{harrison_history_2014,
	title = {History of {Interactive} {Theorem} {Proving}},
	volume = {9},
	isbn = {978-0-444-51624-4},
	url = {https://linkinghub.elsevier.com/retrieve/pii/B9780444516244500046},
	language = {en},
	urldate = {2021-08-19},
	booktitle = {Handbook of the {History} of {Logic}},
	publisher = {Elsevier},
	author = {Harrison, John and Urban, Josef and Wiedijk, Freek},
	year = {2014},
	doi = {10.1016/B978-0-444-51624-4.50004-6},
	keywords = {history, survey, theorem prover},
	pages = {135--214},
}

{"_id":"26xpgY8Jqo8CpfzSr","bibbaseid":"harrison-urban-wiedijk-historyofinteractivetheoremproving-2014","author_short":["Harrison, J.","Urban, J.","Wiedijk, F."],"bibdata":{"bibtype":"incollection","type":"incollection","title":"History of Interactive Theorem Proving","volume":"9","isbn":"978-0-444-51624-4","url":"https://linkinghub.elsevier.com/retrieve/pii/B9780444516244500046","language":"en","urldate":"2021-08-19","booktitle":"Handbook of the History of Logic","publisher":"Elsevier","author":[{"propositions":[],"lastnames":["Harrison"],"firstnames":["John"],"suffixes":[]},{"propositions":[],"lastnames":["Urban"],"firstnames":["Josef"],"suffixes":[]},{"propositions":[],"lastnames":["Wiedijk"],"firstnames":["Freek"],"suffixes":[]}],"year":"2014","doi":"10.1016/B978-0-444-51624-4.50004-6","keywords":"history, survey, theorem prover","pages":"135–214","bibtex":"@incollection{harrison_history_2014,\n\ttitle = {History of {Interactive} {Theorem} {Proving}},\n\tvolume = {9},\n\tisbn = {978-0-444-51624-4},\n\turl = {https://linkinghub.elsevier.com/retrieve/pii/B9780444516244500046},\n\tlanguage = {en},\n\turldate = {2021-08-19},\n\tbooktitle = {Handbook of the {History} of {Logic}},\n\tpublisher = {Elsevier},\n\tauthor = {Harrison, John and Urban, Josef and Wiedijk, Freek},\n\tyear = {2014},\n\tdoi = {10.1016/B978-0-444-51624-4.50004-6},\n\tkeywords = {history, survey, theorem prover},\n\tpages = {135--214},\n}\n\n","author_short":["Harrison, J.","Urban, J.","Wiedijk, F."],"key":"harrison_history_2014","id":"harrison_history_2014","bibbaseid":"harrison-urban-wiedijk-historyofinteractivetheoremproving-2014","role":"author","urls":{"Paper":"https://linkinghub.elsevier.com/retrieve/pii/B9780444516244500046"},"keyword":["history","survey","theorem prover"],"metadata":{"authorlinks":{}},"html":""},"bibtype":"incollection","biburl":"https://bibbase.org/zotero/andreg-p","dataSources":["QGwcHf7xnb5mCCQi7"],"keywords":["history","survey","theorem prover"],"search_terms":["history","interactive","theorem","proving","harrison","urban","wiedijk"],"title":"History of Interactive Theorem Proving","year":2014}