Publications

A Coq Formalization of Finitely Presented Modules, Cyril Cohen and Anders Mörtberg.
Accepted for publication in the proceedings of ITP 2014.
[ preprint (prior to correction) ]

Refinements for free!, Cyril Cohen, Maxime Dénès, Anders Mörtberg.
In the proceedings of CPP 2013.
[Springer  PDF  BibTeX]

Pragmatic Quotient Types in Coq, Cyril Cohen.
In the proceedings of ITP 2013.
[Springer  PDF  BibTeX]

A MachineChecked 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 and Laurent Thery.
In the proceedings of ITP 2013.
[Inria HAL  Springer  BibTeX]

A constructive version of Laplace’s proof on the existence of complex roots, Cyril Cohen and Thierry Coquand.
In Journal of Algebra (2013)
[Inria HAL  Elsevier  PDF  BibTeX]

Construction of real algebraic numbers in Coq, Cyril Cohen.
In the proceedings of ITP 2012
[Inria HAL  Springer  PDF  BibTeX]

Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination, Cyril Cohen and Assia Mahboubi.
In LMCS 2012
[Inria HAL  LMCS  PDF  BibTeX]

Construction des nombres algébriques réels en Coq (in french),
Cyril Cohen.
In the proceedings of JFLA 2012
[Inria HAL  PDF  BibTeX]

A formal quantifier elimination for algebraically closed fields,
Cyril Cohen and Assia Mahboubi.
In the proceedings of CICM 2010, Calculemus
[Inria HAL  Springer] [PDF  BibTeX]
Talks and Seminars

Refinements for free!
[ Slides ] presented at Imperial College on May 8, 2014.

CoqEAL – the Coq Effective Algebra Library
[ Slides ] presented at SMC 2014, Week 4

Refinements for free!
[ Slides ] presented at Proglog seminar

A Coq formalization of finitely presented modules
[ Slides ] presented at Marelle seminar

Why so much fuss over equality?
[ Slides ] presented at Chalmers CS Division’s Summer meeting 2013

Reasoning about big enough numbers in Coq
[Proposal  Slides  Demo] presented at the “4th Coq Workshop” in Princeton in August 2012

A construction of the discrete field of real algebraic numbers in Coq
[ Slides ] presented at the Brouwer seminar in Radboud University Nijmegen in March 2012

Formalisation de l’élimination des quantificateurs pour les corps réels clos en COQ
[ Slides ] presented at Université Rennes 1 – IRMAR in February 2012

Construction of real algebraic numbers in Coq
[ Slides ] presented at MAP 2011 and at journées GeoCalLAC

Quantifier elimination in real closed fields : a formal proof
[ Slides ] presented at TYPES 2011

Formalized foundations of polynomial real analysis
[ Slides ] presented at TYPES 2010
PhD Thesis

Formalized algebraic numbers: construction and firstorder theory, Cyril Cohen.
PhD Thesis, November 20, 2012.
[ PDF  Slides  BibTeX]
Unpublished
Old Intership reports
(Coming, someday)
This page was last updated at
20141201 03:52:16 +0100