Publications
See HAL Publication listTalks and Seminars
(not updated since 2015)-
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 GeoCal-LAC
-
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 first-order theory, Cyril Cohen.
PhD Thesis, November 20, 2012.
[ PDF | Slides | BibTeX]
Unpublished
Old Intership reports
(Coming, someday)