Cyril Cohen

ORCID

Publication Activity (10 Years)

Years Active: 2010-2024
Publications (10 Years): 21

Top Venues

École Polytechnique, Palaiseau, France (PHD)

Education History

École Polytechnique, Palaiseau, France

PHD

Publications

Cyril Cohen, Enzo Crance, Assia Mahboubi
Trocq: Proof Transfer for Free, With or Without Univalence. ESOP (1) (2024)
Cyril Cohen, Enzo Crance, Assia Mahboubi
Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence. ESOP (1) (2024)
Cyril Cohen, Kazuhiko Sakaguchi
A bargain for mergesorts (functional pearl) - How to prove your mergesort correct and stable, almost for free. CoRR (2024)
Reynald Affeldt, Cyril Cohen
Measure Construction by Extension in Dependent Type Theory with Application to Integration. J. Autom. Reason. 67 (3) (2023)
Cyril Cohen, Enzo Crance, Assia Mahboubi
Trocq: Proof Transfer for Free, With or Without Univalence. CoRR (2023)
Reynald Affeldt, Cyril Cohen, Ayumu Saito
Semantics of Probabilistic Programs using s-Finite Kernels in Coq. CPP (2023)
Reynald Affeldt, Cyril Cohen
Measure Construction by Extension in Dependent Type Theory with Application to Integration. CoRR (2022)
Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub
Unsolvability of the Quintic Formalized in Dependent Type Theory. ITP (2021)
Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi
Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. IJCAR (2) (2020)
Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi
Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description). FSCD (2020)
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter
The MetaCoq Project. J. Autom. Reason. 64 (5) (2020)
Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry
Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. ITP (2019)
Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau
Towards Certified Meta-Programming with Typed Template-Coq. ITP (2018)
Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry
Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle. CoRR (2018)
Reynald Affeldt, Cyril Cohen, Damien Rouhling
Formalization Techniques for Asymptotic Reasoning in Classical Analysis. J. Formaliz. Reason. 11 (1) (2018)
Cyril Cohen, Damien Rouhling
A Formal Proof in Coq of LaSalle's Invariance Principle. ITP (2017)
Reynald Affeldt, Cyril Cohen
Formal foundations of 3D geometry to model robot manipulators. CPP (2017)
Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. FLAP 4 (10) (2017)
Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, Vincent Siles
Formalized linear algebra over Elementary Divisor Rings in Coq. Log. Methods Comput. Sci. 12 (2) (2016)
Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
Cubical Type Theory: a constructive interpretation of the univalence axiom. CoRR (2016)
Cyril Cohen, Boris Djalal
Formalization of a newton series representation of polynomials. CPP (2016)
Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. TYPES (2015)
Cyril Cohen, Anders Mörtberg
A Coq Formalization of Finitely Presented Modules. ITP (2014)
Cyril Cohen, Maxime Dénès, Anders Mörtberg
Refinements for Free! CPP (2013)
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry
A Machine-Checked Proof of the Odd Order Theorem. ITP (2013)
Cyril Cohen
Pragmatic Quotient Types in Coq. ITP (2013)
Cyril Cohen
Construction of Real Algebraic Numbers in Coq. ITP (2012)
Cyril Cohen, Assia Mahboubi
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination Log. Methods Comput. Sci. 8 (1) (2012)
Cyril Cohen, Assia Mahboubi
A Formal Quantifier Elimination for Algebraically Closed Fields. AISC/MKM/Calculemus (2010)

Cyril Cohen.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Cyril Cohen