Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
Using Small Scale Automation to Improve Both Accessibility and Readability of Formal Proofs in Geometry, Automated Deduction in Geometry 2014, pp.1-19, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-00989781
From Tarski to Hilbert, Lecture Notes in Computer Science, vol.7993, pp.89-109, 2012. ,
DOI : 10.1007/978-3-642-40672-0_7
URL : https://hal.archives-ouvertes.fr/hal-00727117
Coq, un outil pour l'enseignement. Une exp??rience avec les ??tudiants du DESS D??veloppement de logiciels s??rs, Techniques et sciences informatiques, vol.24, issue.9, pp.1139-1160, 2005. ,
DOI : 10.3166/tsi.24.1139-1160
URL : https://hal.archives-ouvertes.fr/hal-01125076
Formalisation en Coq et visualisation d'un cours de g??om??trie pour le lyc??e, Techniques et sciences informatiques, vol.24, issue.9, pp.1113-1138, 2005. ,
DOI : 10.3166/tsi.24.1113-1138
Teaching Formal Methods and Discrete Mathematics, Proceedings 1st Workshop on Formal Integrated Development Environment, pp.30-43, 2014. ,
DOI : 10.4204/EPTCS.149.4
URL : https://hal.archives-ouvertes.fr/hal-01203024
Coquelicot passe le bac Exposé invité, disponible à https, Journées Francophones des Langages Applicatifs (JFLA), 2014. ,
Mechanical Theorem Proving in Tarski???s Geometry, Automated Deduction in Geometry, ADG 2006. Revised Papers, pp.139-156, 2007. ,
DOI : 10.1007/978-3-540-77356-6_9
Metamathematische Methoden in der Geometrie, 1983. ,
DOI : 10.1007/978-3-642-69418-9
Axiomatique sur les angles, Parameter Point : Set. Definition Point_equal := @eq Point. Parameter Point_col : Point -> Point -> Point -> Prop ,