The Three Gap Theorem (Steinhaus Conjecture). - Micaela Mayero (TYPES, 1999)

Field, une procédure de décision pour les nombres réels en Coq. - David Delahaye; Micaela Mayero (JFLA, 2001)

Using Theorem Proving for Numerical Analysis (Correctness Proof of an Automatic Differentiation Algorithm). - Micaela Mayero (TPHOLs, 2002)

Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant - David Delahaye; Micaela Mayero (CoRR, 2005)

Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System. - David Delahaye; Micaela Mayero (Calculemus, 2005)

Dealing with algebraic expressions over a field in Coq using Maple. - David Delahaye; Micaela Mayero (J. Symb. Comput., 2005)

The Three Gap Theorem (Steinhauss Conjecture) - Micaela Mayero (CoRR, 2006)

Experimenting Formal Proofs of Petri Nets Refinements. - Christine Choppy; Micaela Mayero; Laure Petrucci (Refine@FM, 2008)

Formal Proof of SCHUR Conjugate Function. - Franck Butelle; Florent Hivert; Micaela Mayero; Frédéric Toumazet (AISC/MKM/Calculemus, 2010)

Formal Proof of a Wave Equation Resolution Scheme: The Method Error. - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (ITP, 2010)

Coloured Petri net refinement specification and correctness proof with Coq. - Christine Choppy; Micaela Mayero; Laure Petrucci (Innov. Syst. Softw. Eng., 2010)

Wave Equation Numerical Resolution: Mathematics and Program - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (CoRR, 2011)

Rigorous Polynomial Approximation Using Taylor Models in Coq. - Nicolas Brisebarre; Mioara Joldes; Érik Martin-Dorel; Micaela Mayero; Jean-Michel Muller; Ioana Pasca; Laurence Rideau; Laurent Théry (NASA Formal Methods, 2012)

Certified, Efficient and Sharp Univariate Taylor Models in COQ. - Érik Martin-Dorel; Laurence Rideau; Laurent Théry; Micaela Mayero; Ioana Pasca (SYNASC, 2013)

Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (J. Autom. Reason., 2013)

Trusting computations: A mechanized proof from partial differential equations to actual program. - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (Comput. Math. Appl., 2014)

Formally Verified Certificate Checkers for Hardest-to-Round Computation. - Érik Martin-Dorel; Guillaume Hanrot; Micaela Mayero; Laurent Théry (J. Autom. Reason., 2015)

A Coq formal proof of the LaxMilgram theorem. - Sylvie Boldo; François Clément; Florian Faissole; Vincent Martin; Micaela Mayero (CPP, 2017)

Formal proof of polynomial-time complexity with quasi-interpretations. - Hugo Férée; Samuel Hym; Micaela Mayero; Jean-Yves Moyen; David Nowak (CPP, 2018)

Lebesgue Induction and Tonelli's Theorem in Coq. - Sylvie Boldo; François Clément; Vincent Martin; Micaela Mayero; Houda Mouhcine (CoRR, 2022)

A Coq Formalization of Lebesgue Integration of Nonnegative Functions. - Sylvie Boldo; François Clément; Florian Faissole; Vincent Martin; Micaela Mayero (J. Autom. Reason., 2022)

A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem. - Sylvie Boldo; François Clément; Vincent Martin; Micaela Mayero; Houda Mouhcine (FM, 2023)

Teaching Divisibility and Binomials with Coq. - Sylvie Boldo; François Clément; David Hamelin; Micaela Mayero; Pierre Rousselin (ThEdu@CADE, 2024)

Maths with Coq in L1, a pedagogical experiment. - Marie Kerjean; Micaela Mayero; Pierre Rousselin (ThEdu@CADE, 2024)