CV de Cyril Cohen

Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, Vincent Siles. Formalized Linear Algebra over Elementary Divisor Rings in Coq. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2016, <10.2168/LMCS-12(2:7)2016>. <hal-01081908>

Cyril Cohen, Thierry Coquand. A constructive version of Laplace's proof on the existence of complex roots. Journal of Algebra, Elsevier, 2013, 381, pp.110-115. <10.1016/j.jalgebra.2013.01.016>. <inria-00592284v2>

Cyril Cohen, Assia Mahboubi. Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (1:02), pp.1-40. <10.2168/LMCS-8 (1:02) 2012>. <inria-00593738v4>

Reynald Affeldt, Cyril Cohen. Formal Foundations of 3D Geometry to Model Robot Manipulators. Conference on Certified Programs and Proofs 2017, Jan 2017, Paris, France. <hal-01414753>

Cyril Cohen, Boris Djalal. Formalization of a Newton Series Representation of Polynomials. Jeremy Avigad and Adam Chlipala. Certified Programs and Proofs, Jan 2016, St Petersburg, Florida, United States. Certified Programs and Proofs, 2016. <hal-01240469>

Cyril Cohen, Anders Mörtberg. A Coq Formalization of Finitely Presented Modules. 5th International Conference, ITP 2014, Jul 2014, Vienna, Austria. pp.193 - 208, 2014, <10.1007/978-3-319-08970-6_13>. <hal-01378905>

Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, et al.. A Machine-Checked Proof of the Odd Order Theorem. Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.163-179, 2013, LNCS. <10.1007/978-3-642-39634-2_14>. <hal-00816699>

Cyril Cohen, Maxime Dénès, Anders Mörtberg. Refinements for Free!. Certified Programs and Proofs, Dec 2013, Melbourne, Australia. pp.147 - 162, 2013, <10.1007/978-3-319-03545-1_10>. <hal-01113453>

Cyril Cohen. Construction of real algebraic numbers in Coq. Lennart Beringer and Amy Felty. ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. Springer, 2012. <hal-00671809v2>

Cyril Cohen. Construction des nombres algébriques réels en Coq. JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France. 2012. <hal-00665965>

Cyril Cohen, Assia Mahboubi. A formal quantifier elimination for algebraically closed fields. Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. Springer, 6167, pp.189-203, 2010, Computer Science; Intelligent Computer Mathematics. <10.1007/978-3-642-14128-7_17>. <inria-00464237v3>

Peter Aczel, Benedikt Ahrens, Thorsten Altenkirch, Steve Awodey, Bruno Barras, et al.. Homotopy Type Theory: Univalent Foundations of Mathematics. Aucun, pp.448, 2013. <hal-00935057>

Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg. Cubical Type Theory: a constructive interpretation of the univalence axiom. Accepted for publication in LIPIcs. 2016. <hal-01378906>

Cyril Cohen. Formalizing real analysis for polynomials. 2010. <inria-00545778>

Cyril Cohen. Formalized algebraic numbers: construction and first-order theory.. Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English. <pastel-00780446>