Cyril Cohen Resume

Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, yannick Forster, et al.. The MetaCoq Project. Journal of Automated Reasoning, Springer Verlag, 2020, ⟨10.1007/s10817-019-09540-0⟩. ⟨hal-02167423⟩

Reynald Affeldt, Cyril Cohen, Damien Rouhling. Formalization Techniques for Asymptotic Reasoning in Classical Analysis. Journal of Formalized Reasoning, ASDD-AlmaDL, 2018. ⟨hal-01719918v3⟩

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, Xavier Allamigeon, yves Bertot, Quentin Canu, Cyril Cohen, et al.. Porting the Mathematical Components library to Hierarchy Builder. the COQ Workshop 2021, Jul 2021, virtuel- Rome, Italy. ⟨hal-03463762⟩

Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-yves Strub. Unsolvability of the Quintic Formalized in Dependent Type Theory. ITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Rome / Virtual, France. ⟨hal-03136002v4⟩

Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, et al.. Competing inheritance paths in dependent type theory: a case study in functional analysis. IJCAR 2020 - International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.1-19. ⟨hal-02463336v2⟩

Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi. Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi. FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. pp.34:1--34:21, ⟨10.4230/LIPIcs.FSCD.2020.34⟩. ⟨hal-02478907v5⟩

Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Théry. Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. ITP 2019 - 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. pp.13:1 - 13:19, ⟨10.4230/LIPIcs.ITP.2019.13⟩. ⟨hal-02303987⟩

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.20-39, ⟨10.1007/978-3-319-94821-8_2⟩. ⟨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. Certified Programs and Proofs, Jan 2016, St. Petersburg, Florida, United States. ⟨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. pp.262, ⟨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, ⟨10.1007/978-3-319-08970-6_13⟩. ⟨hal-01378905⟩

Cyril Cohen. Pragmatic Quotient Types in Coq. International Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.16. ⟨hal-01966714⟩

Cyril Cohen, Maxime Dénès, Anders Mörtberg. Refinements for Free!. Certified Programs and Proofs, Dec 2013, Melbourne, Australia. pp.147 - 162, ⟨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. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.163-179, ⟨10.1007/978-3-642-39634-2_14⟩. ⟨hal-00816699⟩

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

Cyril Cohen. Construction of real algebraic numbers in Coq. ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. ⟨hal-00671809v2⟩

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. pp.189-203, ⟨10.1007/978-3-642-14128-7_17⟩. ⟨inria-00464237v3⟩

Cyril Cohen, Théo Zimmermann. A Nix toolbox for reproducible Coq environments, Continuous Integration and artifact reuse. The Coq Workshop, Jul 2021, Virtual, France. ⟨hal-03366644⟩

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. Formalization of a sign determination algorithm in real algebraic geometry. 2021. ⟨hal-03274013⟩

Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Thery. Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle. 2018. ⟨hal-01906155⟩

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⟩