Nombre de documents


CV de Cyril Cohen

Article dans une revue3 documents

Communication dans un congrès11 documents

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

Ouvrage (y compris édition critique et traduction)1 document

  • 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〉

Pré-publication, Document de travail2 documents

  • 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〉

Thèse1 document

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