@inproceedings{DBLP:conf/itp/BernardCMS21,
  author = {Sophie Bernard and Cyril Cohen and Assia Mahboubi and
Pierre{-}Yves Strub},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl = {https://dblp.org/rec/conf/itp/BernardCMS21.bib},
  booktitle = {12th International Conference on Interactive Theorem
Proving, {ITP} 2021, June 29 to July 1, 2021, Rome,
Italy (Virtual Conference)},
  doi = {10.4230/LIPIcs.ITP.2021.8},
  editor = {Liron Cohen and Cezary Kaliszyk},
  isbn = {978-3-95977-188-7},
  pages = {8:1--8:18},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r
Informatik},
  series = {LIPIcs},
  timestamp = {Mon, 21 Jun 2021 14:45:49 +0200},
  title = {Unsolvability of the Quintic Formalized in Dependent
Type Theory},
  url = {https://doi.org/10.4230/LIPIcs.ITP.2021.8},
  volume = {193},
  year = {2021}
}

{"_id":"YxLuJiHaHCYhbj8T3","bibbaseid":"bernard-cohen-mahboubi-strub-unsolvabilityofthequinticformalizedindependenttypetheory-2021","author_short":["Bernard, S.","Cohen, C.","Mahboubi, A.","Strub, P."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Sophie"],"propositions":[],"lastnames":["Bernard"],"suffixes":[]},{"firstnames":["Cyril"],"propositions":[],"lastnames":["Cohen"],"suffixes":[]},{"firstnames":["Assia"],"propositions":[],"lastnames":["Mahboubi"],"suffixes":[]},{"firstnames":["Pierre-Yves"],"propositions":[],"lastnames":["Strub"],"suffixes":[]}],"bibsource":"dblp computer science bibliography, https://dblp.org","biburl":"https://dblp.org/rec/conf/itp/BernardCMS21.bib","booktitle":"12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)","doi":"10.4230/LIPIcs.ITP.2021.8","editor":[{"firstnames":["Liron"],"propositions":[],"lastnames":["Cohen"],"suffixes":[]},{"firstnames":["Cezary"],"propositions":[],"lastnames":["Kaliszyk"],"suffixes":[]}],"isbn":"978-3-95977-188-7","pages":"8:1–8:18","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","series":"LIPIcs","timestamp":"Mon, 21 Jun 2021 14:45:49 +0200","title":"Unsolvability of the Quintic Formalized in Dependent Type Theory","url":"https://doi.org/10.4230/LIPIcs.ITP.2021.8","volume":"193","year":"2021","bibtex":"@inproceedings{DBLP:conf/itp/BernardCMS21,\n author = {Sophie Bernard and Cyril Cohen and Assia Mahboubi and\nPierre{-}Yves Strub},\n bibsource = {dblp computer science bibliography, https://dblp.org},\n biburl = {https://dblp.org/rec/conf/itp/BernardCMS21.bib},\n booktitle = {12th International Conference on Interactive Theorem\nProving, {ITP} 2021, June 29 to July 1, 2021, Rome,\nItaly (Virtual Conference)},\n doi = {10.4230/LIPIcs.ITP.2021.8},\n editor = {Liron Cohen and Cezary Kaliszyk},\n isbn = {978-3-95977-188-7},\n pages = {8:1--8:18},\n publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\\\"{u}}r\nInformatik},\n series = {LIPIcs},\n timestamp = {Mon, 21 Jun 2021 14:45:49 +0200},\n title = {Unsolvability of the Quintic Formalized in Dependent\nType Theory},\n url = {https://doi.org/10.4230/LIPIcs.ITP.2021.8},\n volume = {193},\n year = {2021}\n}\n\n","author_short":["Bernard, S.","Cohen, C.","Mahboubi, A.","Strub, P."],"editor_short":["Cohen, L.","Kaliszyk, C."],"key":"DBLP:conf/itp/BernardCMS21","id":"DBLP:conf/itp/BernardCMS21","bibbaseid":"bernard-cohen-mahboubi-strub-unsolvabilityofthequinticformalizedindependenttypetheory-2021","role":"author","urls":{"Paper":"https://doi.org/10.4230/LIPIcs.ITP.2021.8"},"metadata":{"authorlinks":{}},"html":""},"bibtype":"inproceedings","biburl":"http://www.strub.nu/biblio/strub.bib","dataSources":["q4vBTsWpxooqz6FoB"],"keywords":[],"search_terms":["unsolvability","quintic","formalized","dependent","type","theory","bernard","cohen","mahboubi","strub"],"title":"Unsolvability of the Quintic Formalized in Dependent Type Theory","year":2021}