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〉

Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau. Towards Certified Meta-Programming with Typed Template-Coq. ITP 2018 - 9th Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. pp.1-18, 2018. 〈hal-01809681〉

Cyril Cohen, Damien Rouhling. A Formal Proof in Coq of LaSalle's Invariance Principle. Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. 〈10.1007/978-3-319-66107-0_10〉. 〈hal-01612293〉

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, Thierry Coquand, Simon Huber, Anders Mörtberg. Cubical Type Theory: a constructive interpretation of the univalence axiom. 21st International Conference on Types for Proofs and Programs, May 2015, Tallinn, Estonia. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, pp.262, 2018, 21st International Conference on Types for Proofs and Programs. 〈http://drops.dagstuhl.de/opus/volltexte/2018/8475〉. 〈10.4230/LIPIcs.TYPES.2015.5〉. 〈hal-01378906v2〉

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〉

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〉

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. 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. 〈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〉

Reynald Affeldt, Cyril Cohen, Damien Rouhling. Formalization Techniques for Asymptotic Reasoning in Classical Analysis. 2018. 〈hal-01719918v2〉

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〉