{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:05Z","timestamp":1750221305561,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":38,"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\/3167101","type":"proceedings-article","created":{"date-parts":[[2018,3,16]],"date-time":"2018-03-16T16:10:56Z","timestamp":1521216656000},"page":"28-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["A formal proof in Coq of a control function for the inverted pendulum"],"prefix":"10.1145","author":[{"given":"Damien","family":"Rouhling","sequence":"first","affiliation":[{"name":"University of C\u00f4te d'Azur, France \/ Inria, France"}]}],"member":"320","published-online":{"date-parts":[[2018,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Knepper","author":"Anand Abhishek","year":"2015","unstructured":"Abhishek Anand and Ross A . Knepper . 2015 . ROSCoq: Robots Powered by Constructive Reals. In Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings (Lecture Notes in Computer Science), Christian Urban and Xingyuan Zhang (Eds.), Vol. 9236 . Springer , 34\u201350. Abhishek Anand and Ross A. Knepper. 2015. ROSCoq: Robots Powered by Constructive Reals. In Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings (Lecture Notes in Computer Science), Christian Urban and Xingyuan Zhang (Eds.), Vol. 9236. Springer, 34\u201350."},{"key":"e_1_3_2_1_2_1","volume-title":"ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Lecture Notes in Computer Science","volume":"7998","author":"Blazy Sandrine","year":"2013","unstructured":"Sandrine Blazy , Christine Paulin-Mohring , and David Pichardie ( Eds .). 2013 . Interactive Theorem Proving - 4th International Conference , ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Lecture Notes in Computer Science , Vol. 7998 . Springer. Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). 2013. Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Lecture Notes in Computer Science, Vol. 7998. Springer."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9255-4"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_22"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0181-1"},{"key":"e_1_3_2_1_6_1","unstructured":"Matthew Chan Daniel Ricketts Sorin Lerner and Gregory Malecha. 2016. Formal Verification of Stability Properties of Cyber-physical Systems.  Matthew Chan Daniel Ricketts Sorin Lerner and Gregory Malecha. 2016. Formal Verification of Stability Properties of Cyber-physical Systems."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6911(02)00229-3"},{"key":"e_1_3_2_1_8_1","volume-title":"8th International Conference, ITP 2017, Bras\u00edlia, Brazil, September 26-29, 2017, Proceedings (Lecture Notes in Computer Science), Mauricio AyalaRinc\u00f3n and C\u00e9sar A. Mu\u00f1oz (Eds.)","volume":"10499","author":"Cohen Cyril","year":"2017","unstructured":"Cyril Cohen and Damien Rouhling . 2017 . A Formal Proof in Coq of LaSalle\u2019s Invariance Principle. In Interactive Theorem Proving - 8th International Conference, ITP 2017, Bras\u00edlia, Brazil, September 26-29, 2017, Proceedings (Lecture Notes in Computer Science), Mauricio AyalaRinc\u00f3n and C\u00e9sar A. Mu\u00f1oz (Eds.) , Vol. 10499 . Springer, 148\u2013163. Cyril Cohen and Damien Rouhling. 2017. A Formal Proof in Coq of LaSalle\u2019s Invariance Principle. In Interactive Theorem Proving - 8th International Conference, ITP 2017, Bras\u00edlia, Brazil, September 26-29, 2017, Proceedings (Lecture Notes in Computer Science), Mauricio AyalaRinc\u00f3n and C\u00e9sar A. Mu\u00f1oz (Eds.), Vol. 10499. Springer, 148\u2013163."},{"key":"e_1_3_2_1_9_1","volume-title":"Third International Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings (Lecture Notes in Computer Science), Andrea Asperti, Grzegorz Bancerek, and Andrzej Trybulec (Eds.)","volume":"3119","author":"Cruz-Filipe Lu\u00eds","year":"2004","unstructured":"Lu\u00eds Cruz-Filipe , Herman Geuvers , and Freek Wiedijk . 2004 . C-CoRN, the Constructive Coq Repository at Nijmegen. In Mathematical Knowledge Management , Third International Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings (Lecture Notes in Computer Science), Andrea Asperti, Grzegorz Bancerek, and Andrzej Trybulec (Eds.) , Vol. 3119 . Springer, 88\u2013103. Lu\u00eds Cruz-Filipe, Herman Geuvers, and Freek Wiedijk. 2004. C-CoRN, the Constructive Coq Repository at Nijmegen. In Mathematical Knowledge Management, Third International Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings (Lecture Notes in Computer Science), Andrea Asperti, Grzegorz Bancerek, and Andrzej Trybulec (Eds.), Vol. 3119. Springer, 88\u2013103."},{"key":"e_1_3_2_1_10_1","volume-title":"Pontarlier, France","author":"Delahaye David","year":"2001","unstructured":"David Delahaye and Micaela Mayero . 2001 . Field, une proc\u00e9dure de d\u00e9cision pour les nombres r\u00e9els en Coq. In Journ\u00e9es francophones des langages applicatifs (JFLA\u201901) , Pontarlier, France , Janvier, 2001 (Collection Didactique), Pierre Cast\u00e9ran (Ed.). INRIA, 33\u201348. David Delahaye and Micaela Mayero. 2001. Field, une proc\u00e9dure de d\u00e9cision pour les nombres r\u00e9els en Coq. In Journ\u00e9es francophones des langages applicatifs (JFLA\u201901), Pontarlier, France, Janvier, 2001 (Collection Didactique), Pierre Cast\u00e9ran (Ed.). INRIA, 33\u201348."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SSST.1998.660100"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_36"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_7"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_8"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9250-9"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_15"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Johannes H\u00f6lzl Fabian Immler and Brian Huffman. 2013. Type Classes and Filters for Mathematical Analysis in Isabelle\/HOL See { 2 } 279\u2013294.  Johannes H\u00f6lzl Fabian Immler and Brian Huffman. 2013. Type Classes and Filters for Mathematical Analysis in Isabelle\/HOL See { 2 } 279\u2013294.","DOI":"10.1007\/978-3-642-39634-2_21"},{"key":"e_1_3_2_1_19_1","volume-title":"18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings. Lecture Notes in Computer Science","volume":"3603","author":"Hurd Joe","unstructured":"Joe Hurd and Thomas F . Melham (Eds.). 2005. Theorem Proving in Higher Order Logics , 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings. Lecture Notes in Computer Science , Vol. 3603 . Springer. Joe Hurd and Thomas F. Melham (Eds.). 2005. Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings. Lecture Notes in Computer Science, Vol. 3603. Springer."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_26"},{"volume-title":"Nonlinear Systems","author":"Khalil Hassan K.","key":"e_1_3_2_1_21_1","unstructured":"Hassan K. Khalil . 2002. Nonlinear Systems . Prentice Hall . https: \/\/books.google.fr\/books?id=t_d1QgAACAAJ Hassan K. Khalil. 2002. Nonlinear Systems. Prentice Hall. https: \/\/books.google.fr\/books?id=t_d1QgAACAAJ"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCT.1960.1086720"},{"volume-title":"Diff\u00e9rentiabilit\u00e9 et int\u00e9grabilit\u00e9 en Coq. Application \u00e0 la formule de d\u2019Alembert. In 23\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs","author":"Lelay Catherine","key":"e_1_3_2_1_23_1","unstructured":"Catherine Lelay and Guillaume Melquiond . 2012. Diff\u00e9rentiabilit\u00e9 et int\u00e9grabilit\u00e9 en Coq. Application \u00e0 la formule de d\u2019Alembert. In 23\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs . Carnac, France , 119\u2013133. http:\/\/hal.inria.fr\/hal-00642206\/fr\/ Catherine Lelay and Guillaume Melquiond. 2012. Diff\u00e9rentiabilit\u00e9 et int\u00e9grabilit\u00e9 en Coq. Application \u00e0 la formule de d\u2019Alembert. In 23\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs. Carnac, France, 119\u2013133. http:\/\/hal.inria.fr\/hal-00642206\/fr\/"},{"key":"e_1_3_2_1_24_1","first-page":"203","article-title":"Probl\u00e8me g\u00e9n\u00e9ral de la stabilit\u00e9 du mouvement. Annales de la Facult\u00e9 des sciences de Toulouse","volume":"9","author":"Liapounoff Alexandre","year":"1907","unstructured":"Alexandre Liapounoff . 1907 . Probl\u00e8me g\u00e9n\u00e9ral de la stabilit\u00e9 du mouvement. Annales de la Facult\u00e9 des sciences de Toulouse : Math\u00e9matiques 9 (1907), 203 \u2013 474 . http:\/\/eudml.org\/doc\/72801 Alexandre Liapounoff. 1907. Probl\u00e8me g\u00e9n\u00e9ral de la stabilit\u00e9 du mouvement. Annales de la Facult\u00e9 des sciences de Toulouse : Math\u00e9matiques 9 (1907), 203\u2013474. http:\/\/eudml.org\/doc\/72801","journal-title":"Math\u00e9matiques"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6911(00)00025-6"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_5"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_34"},{"key":"e_1_3_2_1_28_1","volume-title":"Towards Foundational Verification of Cyber-Physical Systems. In 2016 Science of Security for Cyber-Physical Systems Workshop, SOSCYPS@CPSWeek 2016","author":"Malecha Gregory","year":"2016","unstructured":"Gregory Malecha , Daniel Ricketts , Mario M. Alvarez , and Sorin Lerner . 2016 . Towards Foundational Verification of Cyber-Physical Systems. In 2016 Science of Security for Cyber-Physical Systems Workshop, SOSCYPS@CPSWeek 2016 , Vienna, Austria , April 11, 2016. IEEE Computer Society, 1\u20135. Gregory Malecha, Daniel Ricketts, Mario M. Alvarez, and Sorin Lerner. 2016. Towards Foundational Verification of Cyber-Physical Systems. In 2016 Science of Security for Cyber-Physical Systems Workshop, SOSCYPS@CPSWeek 2016, Vienna, Austria, April 11, 2016. IEEE Computer Society, 1\u20135."},{"key":"e_1_3_2_1_30_1","volume-title":"15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings (Lecture Notes in Computer Science), Victor Carre\u00f1o, C\u00e9sar A. Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.)","volume":"2410","author":"Mayero Micaela","year":"2002","unstructured":"Micaela Mayero . 2002 . Using Theorem Proving for Numerical Analysis (Correctness Proof of an Automatic Differentiation Algorithm). In Theorem Proving in Higher Order Logics , 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings (Lecture Notes in Computer Science), Victor Carre\u00f1o, C\u00e9sar A. Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.) , Vol. 2410 . Springer, 246\u2013262. Micaela Mayero. 2002. Using Theorem Proving for Numerical Analysis (Correctness Proof of an Automatic Differentiation Algorithm). In Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings (Lecture Notes in Computer Science), Victor Carre\u00f1o, C\u00e9sar A. Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.), Vol. 2410. Springer, 246\u2013262."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_20"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1459784"},{"key":"e_1_3_2_1_33_1","unstructured":"Ioana Pa\u015fca. 2008. A Formal Verification for Kantorovitch\u2019s Theorem. In Journ\u00e9es Francophones des Langages Applicatifs. http:\/\/hal.inria.fr\/ inria-00202808\/en\/  Ioana Pa\u015fca. 2008. A Formal Verification for Kantorovitch\u2019s Theorem. In Journ\u00e9es Francophones des Langages Applicatifs. http:\/\/hal.inria.fr\/ inria-00202808\/en\/"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000077"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_15"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.1996.570801"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_3_2_1_38_1","volume-title":"Proceedings of the 2002 IEEE International Conference on Robotics and Automation, ICRA 2002","author":"Sugihara Tomomichi","year":"2002","unstructured":"Tomomichi Sugihara , Yoshihiko Nakamura , and Hirochika Inoue . 2002 . Realtime Humanoid Motion Generation through ZMP Manipulation Based on Inverted Pendulum Control . In Proceedings of the 2002 IEEE International Conference on Robotics and Automation, ICRA 2002 , May 11-15, 2002, Washington, DC, USA. IEEE, 1404\u20131409. Tomomichi Sugihara, Yoshihiko Nakamura, and Hirochika Inoue. 2002. Realtime Humanoid Motion Generation through ZMP Manipulation Based on Inverted Pendulum Control. In Proceedings of the 2002 IEEE International Conference on Robotics and Automation, ICRA 2002, May 11-15, 2002, Washington, DC, USA. IEEE, 1404\u20131409."},{"key":"e_1_3_2_1_39_1","unstructured":"The Coq Development Team. 2016. The Coq proof assistant reference manual. http:\/\/coq.inria.fr Version 8.6.  The Coq Development Team. 2016. The Coq proof assistant reference manual. http:\/\/coq.inria.fr Version 8.6."},{"volume-title":"Topology for Analysis","author":"Wilansky Albert","key":"e_1_3_2_1_40_1","unstructured":"Albert Wilansky . 2008. Topology for Analysis . Dover Publ ., New York, NY. http:\/\/cds.cern.ch\/record\/2222525 Albert Wilansky. 2008. Topology for Analysis. Dover Publ., New York, NY. http:\/\/cds.cern.ch\/record\/2222525"}],"event":{"name":"CPP '18: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Los Angeles CA USA","acronym":"CPP '18"},"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\/3167101","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3167101","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\/3167101"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,8]]},"references-count":38,"alternative-id":["10.1145\/3167101","10.1145\/3176245"],"URL":"https:\/\/doi.org\/10.1145\/3167101","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"}}]}}