{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:47:10Z","timestamp":1767926830685,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,18]],"date-time":"2016-01-18T00:00:00Z","timestamp":1453075200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Cofund Action AMAROUT II","award":["#291803"],"award-info":[{"award-number":["#291803"]}]},{"name":"French National Agency for Research (ANR)","award":["FastRelax (ANR-14-CE25-0018-01)"],"award-info":[{"award-number":["FastRelax (ANR-14-CE25-0018-01)"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,18]]},"DOI":"10.1145\/2854065.2854072","type":"proceedings-article","created":{"date-parts":[[2016,1,12]],"date-time":"2016-01-12T13:18:57Z","timestamp":1452604737000},"page":"76-87","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials"],"prefix":"10.1145","author":[{"given":"Sophie","family":"Bernard","sequence":"first","affiliation":[{"name":"Inria, France"}]},{"given":"Yves","family":"Bertot","sequence":"additional","affiliation":[{"name":"Inria, France"}]},{"given":"Laurence","family":"Rideau","sequence":"additional","affiliation":[{"name":"Inria, France"}]},{"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}]}],"member":"320","published-online":{"date-parts":[[2016,1,18]]},"reference":[{"issue":"1","key":"e_1_3_2_1_1_1","first-page":"71","article-title":"Formalizing a proof that e is transcendental","volume":"4","author":"Bingham Jesse","year":"2011","unstructured":"Jesse Bingham . Formalizing a proof that e is transcendental . Journal of Formalized Reasoning , 4 ( 1 ): 71 \u2013 84 , 2011 . Jesse Bingham. Formalizing a proof that e is transcendental. Journal of Formalized Reasoning, 4(1):71\u201384, 2011.","journal-title":"Journal of Formalized Reasoning"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0181-1"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1950.11999585"},{"key":"e_1_3_2_1_6_1","volume-title":"The coq proof assistant","author":"Coq","year":"2008","unstructured":"Coq development team. The coq proof assistant , 2008 . http: \/\/coq.inria.fr. Coq development team. The coq proof assistant, 2008. http: \/\/coq.inria.fr."},{"key":"e_1_3_2_1_7_1","series-title":"LNCS","first-page":"98","volume-title":"Interactive Theorem Proving, ITP2012","author":"D\u00e9n\u00e8s Maxime","year":"2012","unstructured":"Maxime D\u00e9n\u00e8s , Anders M\u00f6rtberg , and Vincent Siles . A refinementbased approach to computational algebra in coq . In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving, ITP2012 , volume 7406 of LNCS , pages 83\u2013 98 , Princeton, USA , Springer , 2012 . Maxime D\u00e9n\u00e8s, Anders M\u00f6rtberg, and Vincent Siles. A refinementbased approach to computational algebra in coq. In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving, ITP2012, volume 7406 of LNCS, pages 83\u201398, Princeton, USA, Springer, 2012."},{"issue":"11","key":"e_1_3_2_1_8_1","first-page":"1382","article-title":"Formal proof\u2014the Four Color Theorem","volume":"55","author":"Gonthier Georges","year":"2008","unstructured":"Georges Gonthier . Formal proof\u2014the Four Color Theorem . Notices of the AMS , 55 ( 11 ): 1382 \u2013 1393 , 2008 . Georges Gonthier. Formal proof\u2014the Four Color Theorem. Notices of the AMS, 55(11):1382\u20131393, 2008.","journal-title":"Notices of the AMS"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"e_1_3_2_1_10_1","volume-title":"Isabelle Workshop 2014","author":"Haftmann Florian","year":"2014","unstructured":"Florian Haftmann , Andreas Lochbihler , and Wolfgang Schreiner . Towards abstract and executable multivariate polynomials in isabelle . Isabelle Workshop 2014 , http:\/\/www.infsec.ethz.ch\/people\/ andreloc\/publications\/haftmann14iw.pdf, 2014 . Florian Haftmann, Andreas Lochbihler, and Wolfgang Schreiner. Towards abstract and executable multivariate polynomials in isabelle. Isabelle Workshop 2014, http:\/\/www.infsec.ethz.ch\/people\/ andreloc\/publications\/haftmann14iw.pdf, 2014."},{"key":"e_1_3_2_1_11_1","first-page":"269","volume-title":"FMCAD","author":"Harrison John","year":"1996","unstructured":"John Harrison . HOL Light : A Tutorial Introduction . In FMCAD , pages 265\u2013 269 , 1996 . John Harrison. HOL Light: A Tutorial Introduction. In FMCAD, pages 265\u2013269, 1996."},{"key":"e_1_3_2_1_12_1","volume-title":"Gauthier-Villars","author":"Hermite Charles","year":"1874","unstructured":"Charles Hermite . Sur la fonction exponentielle . Gauthier-Villars , Paris , 1874 . Charles Hermite. Sur la fonction exponentielle. Gauthier-Villars, Paris, 1874."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/648231.752983"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01446522"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_37"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9256-3"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Tobias\n      Nipkow Lawrence C.\n      Paulson and \n      Markus\n      Wenzel\n    . Isabelle\/\n      HOL\n       \u2014 A \n      Proof\n      Assistant\n       for \n      Higher-Order Logic volume \n  2283\n   of \n  LNCS\n  . \n  Springer 2002\n  .   Tobias Nipkow Lawrence C. Paulson and Markus Wenzel. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic volume 2283 of LNCS. Springer 2002.","DOI":"10.1007\/3-540-45949-9"},{"issue":"8","key":"e_1_3_2_1_18_1","first-page":"469","article-title":"The transcendence of \u03c0","volume":"46","author":"Niven Ivan","year":"1939","unstructured":"Ivan Niven . The transcendence of \u03c0 . American Mathematical Monthly , 46 ( 8 ): 469 \u2013 471 , October 1939 . Ivan Niven. The transcendence of \u03c0. American Mathematical Monthly, 46(8):469\u2013471, October 1939.","journal-title":"American Mathematical Monthly"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1947-08821-2"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026518331905"}],"event":{"name":"CPP 2016: Certified Proofs and Programs","location":"St. Petersburg FL USA","acronym":"CPP 2016","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854072","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2854065.2854072","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:46Z","timestamp":1750225726000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854072"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,18]]},"references-count":19,"alternative-id":["10.1145\/2854065.2854072","10.1145\/2854065"],"URL":"https:\/\/doi.org\/10.1145\/2854065.2854072","relation":{},"subject":[],"published":{"date-parts":[[2016,1,18]]},"assertion":[{"value":"2016-01-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}