@book{bertot_interactive_2004,
	address = {Berlin, Heidelberg},
	series = {Texts in {Theoretical} {Computer} {Science} {An} {EATCS} {Series}},
	title = {Interactive {Theorem} {Proving} and {Program} {Development}},
	isbn = {978-3-642-05880-6},
	url = {http://link.springer.com/10.1007/978-3-662-07964-5},
	urldate = {2021-08-13},
	publisher = {Springer Berlin Heidelberg},
	author = {Bertot, Yves and Castéran, Pierre},
	editor = {Brauer, Wilfried and Rozenberg, Grzegorz and Salomaa, Arto},
	year = {2004},
	doi = {10.1007/978-3-662-07964-5},
	keywords = {coq, specification, theorem prover},
}

{"_id":"erR3esr7eDF7WWfsA","bibbaseid":"bertot-castran-interactivetheoremprovingandprogramdevelopment-2004","authorIDs":[],"author_short":["Bertot, Y.","Castéran, P."],"bibdata":{"bibtype":"book","type":"book","address":"Berlin, Heidelberg","series":"Texts in Theoretical Computer Science An EATCS Series","title":"Interactive Theorem Proving and Program Development","isbn":"978-3-642-05880-6","url":"http://link.springer.com/10.1007/978-3-662-07964-5","urldate":"2021-08-13","publisher":"Springer Berlin Heidelberg","author":[{"propositions":[],"lastnames":["Bertot"],"firstnames":["Yves"],"suffixes":[]},{"propositions":[],"lastnames":["Castéran"],"firstnames":["Pierre"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Brauer"],"firstnames":["Wilfried"],"suffixes":[]},{"propositions":[],"lastnames":["Rozenberg"],"firstnames":["Grzegorz"],"suffixes":[]},{"propositions":[],"lastnames":["Salomaa"],"firstnames":["Arto"],"suffixes":[]}],"year":"2004","doi":"10.1007/978-3-662-07964-5","keywords":"coq, specification, theorem prover","bibtex":"@book{bertot_interactive_2004,\n\taddress = {Berlin, Heidelberg},\n\tseries = {Texts in {Theoretical} {Computer} {Science} {An} {EATCS} {Series}},\n\ttitle = {Interactive {Theorem} {Proving} and {Program} {Development}},\n\tisbn = {978-3-642-05880-6},\n\turl = {http://link.springer.com/10.1007/978-3-662-07964-5},\n\turldate = {2021-08-13},\n\tpublisher = {Springer Berlin Heidelberg},\n\tauthor = {Bertot, Yves and Castéran, Pierre},\n\teditor = {Brauer, Wilfried and Rozenberg, Grzegorz and Salomaa, Arto},\n\tyear = {2004},\n\tdoi = {10.1007/978-3-662-07964-5},\n\tkeywords = {coq, specification, theorem prover},\n}\n\n","author_short":["Bertot, Y.","Castéran, P."],"editor_short":["Brauer, W.","Rozenberg, G.","Salomaa, A."],"key":"bertot_interactive_2004","id":"bertot_interactive_2004","bibbaseid":"bertot-castran-interactivetheoremprovingandprogramdevelopment-2004","role":"author","urls":{"Paper":"http://link.springer.com/10.1007/978-3-662-07964-5"},"keyword":["coq","specification","theorem prover"],"metadata":{"authorlinks":{}},"html":""},"bibtype":"book","creationDate":"2020-10-14T22:29:49.327Z","downloads":0,"keywords":["coq","specification","theorem prover"],"search_terms":["interactive","theorem","proving","program","development","bertot","castéran"],"title":"Interactive Theorem Proving and Program Development","year":2004,"biburl":"https://bibbase.org/zotero/andreg-p","dataSources":["QGwcHf7xnb5mCCQi7"]}