R. Affeldt and C. Cohen, Formal foundations of 3D geometry to model robot manipulators, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs , CPP 2017, 2016.
DOI : 10.1145/3018610.3018629
URL : https://hal.archives-ouvertes.fr/hal-01414753

A. Anand and R. A. Knepper, ROSCoq: Robots Powered by Constructive Reals, 6th International Conference on Interactive Theorem Proving, pp.34-50, 2015.
DOI : 10.1007/978-3-319-22102-1_3

C. Auger, Z. Bouzid, P. Courtieu, S. Tixeuil, and X. Urbain, Certified Impossibility Results for Byzantine-Tolerant Mobile Robots, 15th International Symposium on Stabilization, Safety, and Security of Distributed Systems, pp.178-190, 2013.
DOI : 10.1007/978-3-319-03089-0_13
URL : https://hal.archives-ouvertes.fr/hal-00834633

C. Cohen, Construction of Real Algebraic Numbers in Coq, 3rd International Conference on Interactive Theorem Proving, pp.67-82, 2012.
DOI : 10.1007/978-3-642-32347-8_6
URL : https://hal.archives-ouvertes.fr/hal-00671809

C. Cohen, Formalized algebraic numbers: construction and firstorder theory, Ecole Polytechnique X, 2012.
URL : https://hal.archives-ouvertes.fr/pastel-00780446

P. Courtieu, L. Rieg, S. Tixeuil, and X. Urbain, Impossibility of gathering, a certification, Information Processing Letters, vol.115, issue.3, pp.447-452, 2015.
DOI : 10.1016/j.ipl.2014.11.001
URL : https://hal.archives-ouvertes.fr/hal-01122869

P. Courtieu, L. Rieg, S. Tixeuil, and X. Urbain, Certified Universal Gathering in $$\mathbb {R} ^2$$ for Oblivious Mobile Robots, 30th International Symposium on Distributed Computing (DISC 2016), pp.187-200, 2016.
DOI : 10.1007/978-3-319-25258-2_22

L. Cruz-filipe, H. Geuvers, and F. Wiedijk, C-CoRN, the Constructive Coq Repository at Nijmegen, 3rd International Conference on Mathematical Knowledge Management, pp.88-103, 2004.
DOI : 10.1007/3-540-45620-1_12

M. Dénès, Étude formelle d'algorithmes efficaces en algèbre linéaire, 2013.

M. Dénès, A. Mörtberg, and V. Siles, A refinement-based approach to computational algebra in Coq, 3rd International Conference on Interactive Theorem Proving (ITP 2012), pp.83-98, 2012.

B. Farooq, O. Hasan, and S. Iqbal, Formal Kinematic Analysis of the Two-Link Planar Manipulator, 15th International Conference on Formal Engineering Methods (ICFEM 2013), pp.347-362, 2013.
DOI : 10.1007/978-3-642-41202-8_23

F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging Mathematical Structures, 22nd International Conference on Theorem Proving in Higher Order Logics, 2009.
DOI : 10.1007/978-3-540-68103-8_11
URL : https://hal.archives-ouvertes.fr/inria-00368403

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A machinechecked proof of the odd order theorem, 4th International Conference on Interactive Theorem Proving (ITP 2013), pp.163-179, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00816699

J. Harrison, The HOL Light Theory of Euclidean Space, Journal of Automated Reasoning, vol.4, issue.2, pp.173-190, 2013.
DOI : 10.1007/s10817-012-9250-9

H. Herencia-zapana, R. Jobredeaux, S. Owre, P. Garoche, E. Feron et al., PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL, 4th International Symposium NASA Formal Methods, pp.147-161, 2012.
DOI : 10.1007/978-3-642-28891-3_15

C. Kaliszyk and R. O. Connor, Computing with classical real numbers

R. Krebbers and B. Spitters, Type classes for efficient exact real arithmetic in Coq, Logical Methods in Computer Science, vol.9, issue.1, 2011.
DOI : 10.2168/LMCS-9(1:1)2013

S. Ma, Z. Shi, Z. Shao, Y. Guan, L. Li et al., Higher-Order Logic Formalization of Conformal Geometric Algebra and its Application in Verifying a Robotic Manipulation Algorithm, Advances in Applied Clifford Algebras, pp.1305-1330, 2016.
DOI : 10.1007/s00006-016-0650-5

R. M. Murray, Z. Li, and S. S. Sastry, A Mathematical Introduction to Robotic Manipulation, 1994.

B. O. Neill, Elementary Differential Geometry, 1966.

F. C. Park and K. Lynch, Introduction to robotics: Mechanics, planning , and control, 2012.

B. Spitters and E. Van-der-weegen, Type classes for mathematics in type theory, Mathematical Structures in Computer Science, vol.2, issue.04, pp.795-825, 2011.
DOI : 10.1007/3-540-48256-3_10

M. W. Spong, S. Hutchinson, and M. Vidyasagar, Robot Modeling and Control, 2006.

D. Walter, H. Täubig, and C. Lüth, Experiences in Applying Formal Verification in Robotics, 29th International Conference on Computer Safety, Reliability, and Security, pp.347-360, 2010.
DOI : 10.1007/978-3-642-15651-9_26