Skip to Main content Skip to Navigation

pastel-00780446v1  Theses
Cyril Cohen. Formalized algebraic numbers: construction and first-order theory.
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English
inria-00464237v3  Conference papers
Cyril CohenAssia 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⟩
hal-00671809v2  Conference papers
Cyril Cohen. Construction of real algebraic numbers in Coq
ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States
inria-00593738v4  Journal articles
Cyril CohenAssia 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⟩
hal-00665965v1  Conference papers
Cyril Cohen. Construction des nombres algébriques réels en Coq
JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France
hal-00816699v1  Conference papers
Georges GonthierAndrea AspertiJeremy AvigadYves BertotCyril 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-01081908v1  Journal articles
Guillaume CanoCyril CohenMaxime DénèsAnders MörtbergVincent 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-01240469v1  Conference papers
Cyril CohenBoris Djalal. Formalization of a Newton Series Representation of Polynomials
Certified Programs and Proofs, Jan 2016, St. Petersburg, Florida, United States
hal-01966714v1  Conference papers
Cyril Cohen. Pragmatic Quotient Types in Coq
International Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.16
hal-01414753v1  Conference papers
Reynald AffeldtCyril Cohen. Formal Foundations of 3D Geometry to Model Robot Manipulators
Conference on Certified Programs and Proofs 2017, Jan 2017, Paris, France
hal-01113453v1  Conference papers
Cyril CohenMaxime DénèsAnders 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-01378906v2  Conference papers
Cyril CohenThierry CoquandSimon HuberAnders 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-02303987v1  Conference papers
Ran ChenCyril CohenJean-Jacques LevyStephan MerzLaurent 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-02167423v1  Journal articles
Matthieu SozeauAbhishek AnandSimon BoulierCyril CohenYannick Forster et al.  The MetaCoq Project
Journal of Automated Reasoning, Springer Verlag, 2020, ⟨10.1007/s10817-019-09540-0⟩
hal-01809681v1  Conference papers
Abhishek AnandSimon BoulierCyril CohenMatthieu SozeauNicolas 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-02463336v2  Conference papers
Reynald AffeldtCyril CohenMarie KerjeanAssia MahboubiDamien 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-02478907v5  Conference papers
Cyril CohenKazuhiko SakaguchiEnrico Tassi. Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Jun 2020, Paris, France. pp.34:1--34:21