Cyril Cohen

According to our database, Cyril Cohen authored at least 26 papers between 2010 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2024

A bargain for mergesorts (functional pearl) - How to prove your mergesort correct and stable, almost for free.

Cyril Cohen, Kazuhiko Sakaguchi

CoRR, 2024

Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence.

Cyril Cohen, Enzo Crance, Assia Mahboubi

Proceedings of the Programming Languages and Systems, 2024

Trocq: Proof Transfer for Free, With or Without Univalence.

Cyril Cohen, Enzo Crance, Assia Mahboubi

Proceedings of the Programming Languages and Systems, 2024

2023

Measure Construction by Extension in Dependent Type Theory with Application to Integration.

Reynald Affeldt, Cyril Cohen

J. Autom. Reason., September, 2023

Semantics of Probabilistic Programs using s-Finite Kernels in Coq.

Reynald Affeldt, Cyril Cohen, Ayumu Saito

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

2021

Unsolvability of the Quintic Formalized in Dependent Type Theory.

Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

2020

The MetaCoq Project.

Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter

J. Autom. Reason., 2020

Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description).

Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis.

Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle.

Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

2018

Formalization Techniques for Asymptotic Reasoning in Classical Analysis.

Reynald Affeldt, Cyril Cohen, Damien Rouhling

J. Formaliz. Reason., 2018

Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle.

Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry

CoRR, 2018

Towards Certified Meta-Programming with Typed Template-Coq.

Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017

Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom.

Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg

FLAP, 2017

A Formal Proof in Coq of LaSalle's Invariance Principle.

Cyril Cohen, Damien Rouhling

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

Formal foundations of 3D geometry to model robot manipulators.

Reynald Affeldt, Cyril Cohen

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016

Formalized linear algebra over Elementary Divisor Rings in Coq.

Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, Vincent Siles

Log. Methods Comput. Sci., 2016

Formalization of a newton series representation of polynomials.

Cyril Cohen, Boris Djalal

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2014

A Coq Formalization of Finitely Presented Modules.

Cyril Cohen, Anders Mörtberg

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013

A Machine-Checked Proof of the Odd Order Theorem.

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

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Pragmatic Quotient Types in Coq.

Cyril Cohen

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Refinements for Free!

Cyril Cohen, Maxime Dénès, Anders Mörtberg

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012

Formalized algebraic numbers: construction and first-order theory. (Formalisation des nombres algébriques : construction et théorie du premier ordre).

Cyril Cohen

PhD thesis, 2012

Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination

Cyril Cohen, Assia Mahboubi

Log. Methods Comput. Sci., 2012

Construction of Real Algebraic Numbers in Coq.

Cyril Cohen

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2010

A Formal Quantifier Elimination for Algebraically Closed Fields.

Cyril Cohen, Assia Mahboubi

Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010