{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:04:06Z","timestamp":1762459446014,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,16]],"date-time":"2017-01-16T00:00:00Z","timestamp":1484524800000},"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":[[2017,1,16]]},"DOI":"10.1145\/3018610.3018629","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T21:20:29Z","timestamp":1482441629000},"page":"30-42","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Formal foundations of 3D geometry to model robot manipulators"],"prefix":"10.1145","author":[{"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[{"name":"AIST, Japan"}]},{"given":"Cyril","family":"Cohen","sequence":"additional","affiliation":[{"name":"Inria, France"}]}],"member":"320","published-online":{"date-parts":[[2017,1,16]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018629"},{"key":"e_1_3_2_1_2_1","series-title":"LNCS","first-page":"190","volume-title":"15th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS","author":"Auger C.","year":"2013","unstructured":"C. Auger , Z. Bouzid , P. Courtieu , S. Tixeuil , and X. Urbain . Certified impossibility results for byzantine-tolerant mobile robots . In 15th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2013 ), Osaka , Japan, November 13\u2013 16, 2013, volume 8255 of LNCS , pages 178\u2013 190 . Springer, Nov. 2013. C. Auger, Z. Bouzid, P. Courtieu, S. Tixeuil, and X. Urbain. Certified impossibility results for byzantine-tolerant mobile robots. In 15th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2013), Osaka, Japan, November 13\u2013 16, 2013, volume 8255 of LNCS, pages 178\u2013190. Springer, Nov. 2013."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2014.11.001"},{"key":"e_1_3_2_1_5_1","series-title":"LNCS","first-page":"200","volume-title":"30th International Symposium on Distributed Computing (DISC","author":"Courtieu P.","year":"2016","unstructured":"P. Courtieu , L. Rieg , S. Tixeuil , and X. Urbain . Certified universal gathering in R 2 for oblivious mobile robots . In 30th International Symposium on Distributed Computing (DISC 2016 ), Paris , France, September 27\u201329, 2016, volume 9888 of LNCS , pages 187\u2013 200 . Springer, Sep. 2016. P. Courtieu, L. Rieg, S. Tixeuil, and X. Urbain. Certified universal gathering in R 2 for oblivious mobile robots. In 30th International Symposium on Distributed Computing (DISC 2016), Paris, France, September 27\u201329, 2016, volume 9888 of LNCS, pages 187\u2013200. Springer, Sep. 2016."},{"key":"e_1_3_2_1_6_1","series-title":"LNCS","first-page":"103","volume-title":"3rd International Conference on Mathematical Knowledge Management (MKM","author":"Cruz-Filipe L.","year":"2004","unstructured":"L. Cruz-Filipe , H. Geuvers , and F. Wiedijk . C-CoRN: the constructive Coq repository at Nijmegen . In 3rd International Conference on Mathematical Knowledge Management (MKM 2004 ), Bialowieza , Poland, September 19\u201321, 2004, volume 3119 of LNCS , pages 88\u2013 103 . Springer, 2004. L. Cruz-Filipe, H. Geuvers, and F. Wiedijk. C-CoRN: the constructive Coq repository at Nijmegen. In 3rd International Conference on Mathematical Knowledge Management (MKM 2004), Bialowieza, Poland, September 19\u201321, 2004, volume 3119 of LNCS, pages 88\u2013103. Springer, 2004."},{"key":"e_1_3_2_1_8_1","series-title":"LNCS","first-page":"98","volume-title":"3rd International Conference on Interactive Theorem Proving (ITP","author":"D\u00e9n\u00e8s M.","year":"2012","unstructured":"M. D\u00e9n\u00e8s , A. M\u00f6rtberg , and V. Siles . A refinement-based approach to computational algebra in Coq . In 3rd International Conference on Interactive Theorem Proving (ITP 2012 ), Princeton, NJ , USA, August 13\u201315, 2012, volume 7406 of LNCS , pages 83\u2013 98 . Springer, 2012. M. D\u00e9n\u00e8s, A. M\u00f6rtberg, and V. Siles. A refinement-based approach to computational algebra in Coq. In 3rd International Conference on Interactive Theorem Proving (ITP 2012), Princeton, NJ, USA, August 13\u201315, 2012, volume 7406 of LNCS, pages 83\u201398. Springer, 2012."},{"key":"e_1_3_2_1_9_1","series-title":"LNCS","first-page":"362","volume-title":"15th International Conference on Formal Engineering Methods (ICFEM","author":"Farooq B.","year":"2013","unstructured":"B. Farooq , O. Hasan , and S. Iqbal . Formal kinematic analysis of the two-link planar manipulator . In 15th International Conference on Formal Engineering Methods (ICFEM 2013 ), Queenstown, New Zealand , October 29\u2013November 1, 2013, volume 8144 of LNCS , pages 347\u2013 362 , 2013. B. Farooq, O. Hasan, and S. Iqbal. Formal kinematic analysis of the two-link planar manipulator. In 15th International Conference on Formal Engineering Methods (ICFEM 2013), Queenstown, New Zealand, October 29\u2013November 1, 2013, volume 8144 of LNCS, pages 347\u2013362, 2013."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_23"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9250-9"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_15"},{"key":"e_1_3_2_1_14_1","volume-title":"Computing with classical real numbers. CoRR, abs\/0809.1644","author":"Kaliszyk C.","year":"2008","unstructured":"C. Kaliszyk and R. O\u2019Connor . Computing with classical real numbers. CoRR, abs\/0809.1644 , 2008 . C. Kaliszyk and R. O\u2019Connor. Computing with classical real numbers. CoRR, abs\/0809.1644, 2008."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00006-016-0650-5"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/561828"},{"key":"e_1_3_2_1_17_1","volume-title":"Introduction to robotics: Mechanics, planning, and control. Technical report","author":"Park F. C.","year":"2012","unstructured":"F. C. Park and K. Lynch . Introduction to robotics: Mechanics, planning, and control. Technical report , Seoul National University, 2012 . Course text. B. Siciliano and O. Khatib, editors. Springer Handbook of Robotics. Springer , 2008. F. C. Park and K. Lynch. Introduction to robotics: Mechanics, planning, and control. Technical report, Seoul National University, 2012. Course text. B. Siciliano and O. Khatib, editors. Springer Handbook of Robotics. Springer, 2008."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000119"},{"key":"e_1_3_2_1_19_1","volume-title":"Robot Modeling and Control","author":"Spong M. W.","year":"2006","unstructured":"M. W. Spong , S. Hutchinson , and M. Vidyasagar . Robot Modeling and Control . John Wiley & amp; Sons, 2006 . M. W. Spong, S. Hutchinson, and M. Vidyasagar. Robot Modeling and Control. John Wiley & Sons, 2006."},{"key":"e_1_3_2_1_20_1","unstructured":"The Coq\n      Development Team\n    .\n  Reference manual. Available at http:\/\/coq.inria.fr 1999\n  \u20132016. INRIA. Ver. 8.5pl2. D. Walter H. T\u00e4ubig and C. L\u00fcth. Experiences in applying formal verification in robotics. In 29th International Conference on Computer Safety Reliability and Security (SAFECOMP 2010) Vienna Austria September 14\u201317 2010 volume \n  6351\n   of \n  LNCS pages 347\u2013\n  360 2010.   The Coq Development Team. Reference manual. Available at http:\/\/coq.inria.fr 1999\u20132016. INRIA. Ver. 8.5pl2. D. Walter H. T\u00e4ubig and C. L\u00fcth. Experiences in applying formal verification in robotics. In 29th International Conference on Computer Safety Reliability and Security (SAFECOMP 2010) Vienna Austria September 14\u201317 2010 volume 6351 of LNCS pages 347\u2013360 2010."}],"event":{"name":"CPP '17: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Paris France","acronym":"CPP '17"},"container-title":["Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018610.3018629","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3018610.3018629","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:23:59Z","timestamp":1750220639000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018610.3018629"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,16]]},"references-count":19,"alternative-id":["10.1145\/3018610.3018629","10.1145\/3018610"],"URL":"https:\/\/doi.org\/10.1145\/3018610.3018629","relation":{},"subject":[],"published":{"date-parts":[[2017,1,16]]},"assertion":[{"value":"2017-01-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}