{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:44:09Z","timestamp":1767926649880,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,8]],"date-time":"2018-01-08T00:00:00Z","timestamp":1515369600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,1,8]]},"DOI":"10.1145\/3167099","type":"proceedings-article","created":{"date-parts":[[2018,3,16]],"date-time":"2018-03-16T16:10:56Z","timestamp":1521216656000},"page":"240-251","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A constructive formalisation of Semi-algebraic sets and functions"],"prefix":"10.1145","author":[{"given":"Boris","family":"Djalal","sequence":"first","affiliation":[{"name":"Inria, France"}]}],"member":"320","published-online":{"date-parts":[[2018,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"J. R. Johnson B. F. Caviness (Ed.). 1998. Quantifier Elimination and Cylindrical Algebraic Decomposition.  J. R. Johnson B. F. Caviness (Ed.). 1998. Quantifier Elimination and Cylindrical Algebraic Decomposition."},{"key":"e_1_3_2_1_2_1","volume-title":"Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics)","author":"Basu Saugata"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/968708.968710"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11832225_11"},{"key":"e_1_3_2_1_5_1","unstructured":"B.F. Caviness and J.R. Johnson. 2012. Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer Vienna. https:\/\/books.google. fr\/books?id=vu-pCAAAQBAJ  B.F. Caviness and J.R. Johnson. 2012. Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer Vienna. https:\/\/books.google. fr\/books?id=vu-pCAAAQBAJ"},{"key":"e_1_3_2_1_6_1","unstructured":"Cyril Cohen. {n. d.}. Finmap Library. https:\/\/github.com\/math-comp\/ finmap . ({n. d.}). Accessed: 07\/04\/2017.  Cyril Cohen. {n. d.}. Finmap Library. https:\/\/github.com\/math-comp\/ finmap . ({n. d.}). Accessed: 07\/04\/2017."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Cyril Cohen. 2012. Construction of real algebraic numbers in Coq. (2012).  Cyril Cohen. 2012. Construction of real algebraic numbers in Coq. (2012).","DOI":"10.1007\/978-3-642-32347-8_6"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_17"},{"key":"e_1_3_2_1_9_1","volume-title":"Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Logical Methods in Computer Science 8, 1","author":"Cohen Cyril","year":"2012"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693166"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(96)00102-8"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/646524.694722"},{"key":"e_1_3_2_1_13_1","volume-title":"Formalizing Basic First Order Model Theory. In Theorem Proving in Higher Order Logics: 11th International Conference, TPHOLs\u201998 (September\/October 1998)","volume":"1497","author":"Harrison John","year":"1998"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"Harrison John","DOI":"10.1017\/CBO9780511576430"},{"key":"e_1_3_2_1_15_1","volume-title":"Theorem Proving with the Real Numbers","author":"Harrison John","edition":"1"},{"key":"e_1_3_2_1_17_1","article-title":"Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle\/HOL","author":"Li Wenda","year":"2017","journal-title":"Journal of Automated Reasoning (08"},{"key":"e_1_3_2_1_18_1","volume-title":"Paulson","author":"Li Wenda","year":"2016"},{"key":"e_1_3_2_1_19_1","unstructured":"Assia Mahboubi. {n. d.}. lstcoq.sty file which defines a Coq - SSReflect style for listings in Latex. https:\/\/hal.inria.fr\/file\/index\/docid\/611757\/ filename\/lstcoq.sty . ({n. d.}). Accessed: 08\/02\/2017.  Assia Mahboubi. {n. d.}. lstcoq.sty file which defines a Coq - SSReflect style for listings in Latex. https:\/\/hal.inria.fr\/file\/index\/docid\/611757\/ filename\/lstcoq.sty . ({n. d.}). Accessed: 08\/02\/2017."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950600586X"},{"key":"e_1_3_2_1_22_1","unstructured":"Assia Mahboubi and Enrico Tassi. {n. d.}. Mathematical Components. https:\/\/math-comp.github.io\/mcb\/ . ({n. d.}). Accessed: 06\/04\/2017.  Assia Mahboubi and Enrico Tassi. {n. d.}. Mathematical Components. https:\/\/math-comp.github.io\/mcb\/ . ({n. d.}). Accessed: 06\/04\/2017."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9320-x"},{"key":"e_1_3_2_1_24_1","volume-title":"Tools for Practical Software Verification, LASER, International Summer School","author":"Paulin-Mohring Christine","year":"2011"},{"key":"e_1_3_2_1_25_1","volume-title":"A decision method for elementary algebra and geometry. Bull. Amer. Math. Soc. 59","author":"Tarski Alfred","year":"1951"},{"key":"e_1_3_2_1_26_1","unstructured":"Wikipedia. {n. d.}. CAD. https:\/\/en.wikipedia.org\/wiki\/Cylindrical_ algebraic_decomposition . ({n. d.}). Accessed: 11\/04\/2017.  Wikipedia. {n. d.}. CAD. https:\/\/en.wikipedia.org\/wiki\/Cylindrical_ algebraic_decomposition . ({n. d.}). Accessed: 11\/04\/2017."}],"event":{"name":"CPP '18: Certified Proofs and Programs","location":"Los Angeles CA USA","acronym":"CPP '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167099","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3167099","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:28Z","timestamp":1750212808000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167099"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,8]]},"references-count":24,"alternative-id":["10.1145\/3167099","10.1145\/3176245"],"URL":"https:\/\/doi.org\/10.1145\/3167099","relation":{},"subject":[],"published":{"date-parts":[[2018,1,8]]},"assertion":[{"value":"2018-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}