@inproceedings{DBLP:conf/lpar/JouannaudS17,
  author = {Jean{-}Pierre Jouannaud and Pierre{-}Yves Strub},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl = {https://dblp.org/rec/conf/lpar/JouannaudS17.bib},
  booktitle = {LPAR-21, 21st International Conference on Logic for
Programming, Artificial Intelligence and Reasoning,
Maun, Botswana, May 7-12, 2017},
  doi = {10.29007/bjpg},
  editor = {Thomas Eiter and David Sands},
  pages = {474--489},
  publisher = {EasyChair},
  series = {EPiC Series in Computing},
  timestamp = {Sun, 15 Aug 2021 01:00:00 +0200},
  title = {Coq without Type Casts: {A} Complete Proof of Coq
Modulo Theory},
  url = {https://doi.org/10.29007/bjpg},
  volume = {46},
  year = {2017}
}

{"_id":"LSZTdoa2CWMkQfXsS","bibbaseid":"jouannaud-strub-coqwithouttypecastsacompleteproofofcoqmodulotheory-2017","downloads":2,"creationDate":"2017-07-26T06:50:00.560Z","title":"Coq without Type Casts: A Complete Proof of Coq Modulo Theory","author_short":["Jouannaud, J.","Strub, P."],"year":2017,"bibtype":"inproceedings","biburl":"http://www.strub.nu/biblio/strub.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Jean-Pierre"],"propositions":[],"lastnames":["Jouannaud"],"suffixes":[]},{"firstnames":["Pierre-Yves"],"propositions":[],"lastnames":["Strub"],"suffixes":[]}],"bibsource":"dblp computer science bibliography, https://dblp.org","biburl":"https://dblp.org/rec/conf/lpar/JouannaudS17.bib","booktitle":"LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017","doi":"10.29007/bjpg","editor":[{"firstnames":["Thomas"],"propositions":[],"lastnames":["Eiter"],"suffixes":[]},{"firstnames":["David"],"propositions":[],"lastnames":["Sands"],"suffixes":[]}],"pages":"474–489","publisher":"EasyChair","series":"EPiC Series in Computing","timestamp":"Sun, 15 Aug 2021 01:00:00 +0200","title":"Coq without Type Casts: A Complete Proof of Coq Modulo Theory","url":"https://doi.org/10.29007/bjpg","volume":"46","year":"2017","bibtex":"@inproceedings{DBLP:conf/lpar/JouannaudS17,\n author = {Jean{-}Pierre Jouannaud and Pierre{-}Yves Strub},\n bibsource = {dblp computer science bibliography, https://dblp.org},\n biburl = {https://dblp.org/rec/conf/lpar/JouannaudS17.bib},\n booktitle = {LPAR-21, 21st International Conference on Logic for\nProgramming, Artificial Intelligence and Reasoning,\nMaun, Botswana, May 7-12, 2017},\n doi = {10.29007/bjpg},\n editor = {Thomas Eiter and David Sands},\n pages = {474--489},\n publisher = {EasyChair},\n series = {EPiC Series in Computing},\n timestamp = {Sun, 15 Aug 2021 01:00:00 +0200},\n title = {Coq without Type Casts: {A} Complete Proof of Coq\nModulo Theory},\n url = {https://doi.org/10.29007/bjpg},\n volume = {46},\n year = {2017}\n}\n\n","author_short":["Jouannaud, J.","Strub, P."],"editor_short":["Eiter, T.","Sands, D."],"key":"DBLP:conf/lpar/JouannaudS17","id":"DBLP:conf/lpar/JouannaudS17","bibbaseid":"jouannaud-strub-coqwithouttypecastsacompleteproofofcoqmodulotheory-2017","role":"author","urls":{"Paper":"https://doi.org/10.29007/bjpg"},"metadata":{"authorlinks":{"strub, p":"https://www.strub.nu/"}},"downloads":2,"html":""},"search_terms":["coq","without","type","casts","complete","proof","coq","modulo","theory","jouannaud","strub"],"keywords":[],"authorIDs":["EC8a7TQ86pYAoBS7y"],"dataSources":["q4vBTsWpxooqz6FoB"]}