Documentation
Français (FR)

Anglais (EN)

Cyril Cohen

32

Documents

Publications

	Measure Construction by Extension in Dependent Type Theory with Application to Integration Reynald Affeldt , Cyril Cohen Journal of Automated Reasoning, 2023, 67 (3), pp.28. ⟨10.1007/s10817-023-09671-5⟩ Article dans une revue hal-04183173v1
	The MetaCoq Project Matthieu Sozeau , Abhishek Anand , Simon Boulier , Cyril Cohen , Yannick Forster Journal of Automated Reasoning, 2020, ⟨10.1007/s10817-019-09540-0⟩ Article dans une revue hal-02167423v1
	Formalization Techniques for Asymptotic Reasoning in Classical Analysis Reynald Affeldt , Cyril Cohen , Damien Rouhling Journal of Formalized Reasoning, 2018 Article dans une revue hal-01719918v3
	Formalized Linear Algebra over Elementary Divisor Rings in Coq Guillaume Cano , Cyril Cohen , Maxime Dénès , Anders Mörtberg , Vincent Siles Logical Methods in Computer Science, 2016, ⟨10.2168/LMCS-12(2:7)2016⟩ Article dans une revue hal-01081908v1
	A constructive version of Laplace's proof on the existence of complex roots Cyril Cohen , Thierry Coquand Journal of Algebra, 2013, 381, pp.110-115. ⟨10.1016/j.jalgebra.2013.01.016⟩ Article dans une revue inria-00592284v2
	Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination Cyril Cohen , Assia Mahboubi Logical Methods in Computer Science, 2012, 8 (1:02), pp.1-40. ⟨10.2168/LMCS-8(1:02)2012⟩ Article dans une revue inria-00593738v4

	Trocq: Proof Transfer for Free, With or Without Univalence Cyril Cohen , Enzo Crance , Assia Mahboubi ESOP 2024 - 33rd European Symposium on Programming, Apr 2024, Luxembourg, Luxembourg. pp.239-268 Communication dans un congrès hal-04177913v5
	Semantics of Probabilistic Programs using s-Finite Kernels in Coq Reynald Affeldt , Cyril Cohen , Ayumu Saito CPP 2023 - Certified Programs and Proofs, Jan 2023, Boston, United States. ⟨10.1145/3573105.3575691⟩ Communication dans un congrès hal-03917948v1
	Unsolvability of the Quintic Formalized in Dependent Type Theory Sophie Bernard , Cyril Cohen , Assia Mahboubi , Pierre-Yves Strub ITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Rome / Virtual, France Communication dans un congrès hal-03136002v4
	Porting the Mathematical Components library to Hierarchy Builder Reynald Affeldt , Xavier Allamigeon , Yves Bertot , Quentin Canu , Cyril Cohen the COQ Workshop 2021, Jul 2021, virtuel- Rome, Italy Communication dans un congrès hal-03463762v1
	Competing inheritance paths in dependent type theory: a case study in functional analysis Reynald Affeldt , Cyril Cohen , Marie Kerjean , Assia Mahboubi , Damien Rouhling IJCAR 2020 - International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.1-19 Communication dans un congrès hal-02463336v2
	Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi Cyril Cohen , Kazuhiko Sakaguchi , Enrico Tassi 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⟩ Communication dans un congrès hal-02478907v6
	Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle Ran Chen , Cyril Cohen , Jean-Jacques Levy , Stephan Merz , Laurent Théry 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⟩ Communication dans un congrès hal-02303987v1
	Towards Certified Meta-Programming with Typed Template-Coq Abhishek Anand , Simon Boulier , Cyril Cohen , Matthieu Sozeau , Nicolas Tabareau ITP 2018 - 9th Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. pp.20-39, ⟨10.1007/978-3-319-94821-8_2⟩ Communication dans un congrès hal-01809681v1
	A Formal Proof in Coq of LaSalle's Invariance Principle Cyril Cohen , Damien Rouhling Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. ⟨10.1007/978-3-319-66107-0_10⟩ Communication dans un congrès hal-01612293v1
	Formal Foundations of 3D Geometry to Model Robot Manipulators Reynald Affeldt , Cyril Cohen Conference on Certified Programs and Proofs 2017, Jan 2017, Paris, France Communication dans un congrès hal-01414753v1
	Formalization of a Newton Series Representation of Polynomials Cyril Cohen , Boris Djalal Certified Programs and Proofs, Jan 2016, St. Petersburg, Florida, United States Communication dans un congrès hal-01240469v1
	Cubical Type Theory: a constructive interpretation of the univalence axiom Cyril Cohen , Thierry Coquand , Simon Huber , Anders Mörtberg 21st International Conference on Types for Proofs and Programs, May 2015, Tallinn, Estonia. pp.262, ⟨10.4230/LIPIcs.TYPES.2015.5⟩ Communication dans un congrès hal-01378906v2
	A Coq Formalization of Finitely Presented Modules Cyril Cohen , Anders Mörtberg 5th International Conference, ITP 2014, Jul 2014, Vienna, Austria. pp.193 - 208, ⟨10.1007/978-3-319-08970-6_13⟩ Communication dans un congrès hal-01378905v1
	Pragmatic Quotient Types in Coq Cyril Cohen International Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.16 Communication dans un congrès hal-01966714v1
	A Machine-Checked Proof of the Odd Order Theorem Georges Gonthier , Andrea Asperti , Jeremy Avigad , Yves Bertot , Cyril Cohen ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.163-179, ⟨10.1007/978-3-642-39634-2_14⟩ Communication dans un congrès hal-00816699v1
	Refinements for Free! Cyril Cohen , Maxime Dénès , Anders Mörtberg Certified Programs and Proofs, Dec 2013, Melbourne, Australia. pp.147 - 162, ⟨10.1007/978-3-319-03545-1_10⟩ Communication dans un congrès hal-01113453v1
	Construction of real algebraic numbers in Coq Cyril Cohen ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States Communication dans un congrès hal-00671809v2
	Construction des nombres algébriques réels en Coq Cyril Cohen JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France Communication dans un congrès hal-00665965v1
	A formal quantifier elimination for algebraically closed fields Cyril Cohen , Assia Mahboubi 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⟩ Communication dans un congrès inria-00464237v3

	A Nix toolbox for reproducible Coq environments, Continuous Integration and artifact reuse Cyril Cohen , Théo Zimmermann The Coq Workshop, Jul 2021, Virtual, France Document associé à des manifestations scientifiques hal-03366644v1

	Homotopy Type Theory: Univalent Foundations of Mathematics Peter Aczel , Benedikt Ahrens , Thorsten Altenkirch , Steve Awodey , Bruno Barras The Univalent Foundations Program Institute for Advanced Study, pp.1--587, 2013 Ouvrages hal-00935057v1

	Design patterns of hierarchies for order structures Xavier Allamigeon , Quentin Canu , Cyril Cohen , Kazuhiko Sakaguchi , Pierre-Yves Strub 2023 Pré-publication, Document de travail hal-04008820v1
	Formalization of a sign determination algorithm in real algebraic geometry Cyril Cohen 2021 Pré-publication, Document de travail hal-03274013v1
	Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle Ran Chen , Cyril Cohen , Jean-Jacques Levy , Stephan Merz , Laurent Thery 2018 Pré-publication, Document de travail hal-01906155v1
	Formalizing real analysis for polynomials Cyril Cohen 2010 Pré-publication, Document de travail inria-00545778v1

	Formalized algebraic numbers: construction and first-order theory. Cyril Cohen Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English. ⟨NNT : ⟩ Thèse pastel-00780446v1