, ROSCoq: Robots Powered by Constructive Reals, Interactive Theorem Proving -6th International Conference Proceedings (Lecture Notes in Computer Science), pp.34-50978, 2015.
DOI : 10.1007/978-3-319-22102-1_3
, Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program, Journal of Automated Reasoning, vol.200, issue.25???28, pp.423-456, 2013.
DOI : 10.1007/978-1-4899-7278-1
URL : https://hal.archives-ouvertes.fr/hal-00649240
, Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives, Certified Programs and Proofs -Second International Conference Proceedings (Lecture Notes in Computer Science), pp.289-304, 2012.
DOI : 10.1007/978-3-642-35308-6_22
URL : https://hal.archives-ouvertes.fr/hal-00712938
, Coquelicot: A User-Friendly Library of Real Analysis for Coq, Mathematics in Computer Science, vol.24, issue.9, pp.41-62, 2015.
DOI : 10.1109/32.713327
URL : https://hal.archives-ouvertes.fr/hal-00860648
, Formal Verification of Stability Properties of Cyber-physical Systems, 2016.
, Swing-up and stabilization of a cart???pendulum system under restricted cart track length, Systems & Control Letters, vol.47, issue.4, pp.355-364, 2002.
DOI : 10.1016/S0167-6911(02)00229-3
, A Formal Proof in Coq of LaSalle???s Invariance Principle, Interactive Theorem Proving -8th International Conference, pp.148-163978, 2017.
DOI : 10.1007/978-3-540-71067-7_20
, C-CoRN, the Constructive Coq Repository at Nijmegen, Mathematical Knowledge Management, Third International Conference Proceedings (Lecture Notes in Computer Science), pp.88-103, 2004.
DOI : 10.1007/3-540-45620-1_12
URL : http://www.cs.math.ist.utl.pt/ftp/pub/CruzFilipeL/04-CGW-ccorn.ps
, Field, une procédure de décision pour les nombres réels en Coq INRIA, Journées francophones des langages applicatifs (JFLA'01), pp.33-48, 2001.
, MIMO Sliding Mode Control of a RoboticPick and Place" System Modeled as an Inverted Pendulum on a Moving Cart, Proceedings of Thirtieth Southeastern Symposium on System Theory, pp.379-383660100, 1998.
, KeYmaera??X: An Axiomatic Tactical Theorem Prover for Hybrid Systems, Automated Deduction -CADE-25 -25th International Conference on Automated Deduction Proceedings (Lecture Notes in Computer Science), 2015.
DOI : 10.1007/978-3-319-21401-6_36
, A Small Scale Reflection Extension for the Coq system, 2015.
URL : https://hal.archives-ouvertes.fr/inria-00258384
, Proving Equalities in a Commutative Ring Done Right in Coq, See, pp.98-113, 2005.
, A HOL Theory of Euclidean Space, See, pp.114-129, 2005.
, The HOL Light Theory of Euclidean Space, Journal of Automated Reasoning, vol.4, issue.2, pp.173-190, 2013.
DOI : 10.1147/rd.45.0518
, PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL, NASA Formal Methods -4th International Symposium, NFM 2012, pp.147-161, 2012.
DOI : 10.1007/978-3-642-28891-3_15
, Type Classes and Filters for Mathematical Analysis in, pp.279-294978, 2013.
, Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL, Interactive Theorem Proving -Third International Conference Proceedings (Lecture Notes in Computer Science), pp.377-392978, 2012.
DOI : 10.1007/978-3-642-32347-8_26
, Nonlinear Systems, 2002.
URL : https://hal.archives-ouvertes.fr/hal-00811192
, Some Extensions of Liapunov's Second Method, IRE Transactions on Circuit Theory, vol.7, issue.4, pp.520-527, 1960.
DOI : 10.1109/TCT.1960.1086720
, Différentiabilité et intégrabilité en Coq Application à la formule de d'Alembert, 23èmes Journées Francophones des Langages Applicatifs, pp.119-133, 2012.
, Problème général de la stabilité du mouvement Annales de la Faculté des sciences de Toulouse, pp.203-474, 1907.
, Stabilization of the inverted pendulum around its homoclinic orbit, Systems & Control Letters, vol.40, issue.3, pp.197-204, 2000.
DOI : 10.1016/S0167-6911(00)00025-6
, Canonical Structures for the Working Coq User, See, pp.19-34, 2013.
DOI : 10.1007/978-3-642-39634-2_5
, The Picard Algorithm for Ordinary Differential Equations in Coq, See, pp.463-468978, 2013.
, Towards Foundational Verification of Cyber-Physical Systems In 2016 Science of Security for Cyber-Physical Systems Workshop, pp.1-5, 2016.
, Formalisation et automatisation de preuves en analyses réelle et numérique, 2001.
, Using Theorem Proving for Numerical Analysis Correctness Proof of an Automatic Differentiation Algorithm, 2002.
DOI : 10.1007/3-540-45685-6_17
, A Formalized Theory for Verifying Stability and Convergence of Automata in PVS, See, pp.230-245, 2008.
, A Formal Verification for Kantorovitch's Theorem, Journées Francophones des Langages Applicatifs, 2008.
, Formal proofs for theoretical properties of Newton's method, Mathematical Structures in Computer Science, vol.21, issue.04, pp.683-714, 2011.
DOI : 10.1007/978-3-642-03359-9_23
, KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description), Automated Reasoning, 4th International Joint Conference Proceedings (Lecture Notes in Computer Science), pp.171-178, 2008.
DOI : 10.1007/978-3-540-71070-7_15
, Cooperative behavior of a wheeled inverted pendulum for object transportation, Proceedings of IEEE/RSJ International Conference on Intelligent Robots and Systems. IROS '96, pp.396-401570801, 1996.
DOI : 10.1109/IROS.1996.570801
, First-Class Type Classes, See [32, pp.278-293, 2008.
DOI : 10.1007/978-3-540-71067-7_23
URL : http://www.lri.fr/%7Enoury/classes.pdf
, Realtime Humanoid Motion Generation through ZMP Manipulation Based on Inverted Pendulum Control, Proceedings of the, pp.1404-1409, 2002.
DOI : 10.1109/robot.2002.1014740
URL : http://www.ssp.isee.kyushu-u.ac.jp/~sugihara/pub/icra02.pdf
, Topology for Analysis, 2008.