Micaela Mayero

30 papers B 4Misc 1Journal 15Unranked 10

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	A Rocq Formalization of Monomial and Graded Orders. CoRR Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero
2024	—	`conf`	Maths with Coq in L1, a pedagogical experiment. ThEdu@CADE Marie Kerjean, Micaela Mayero, Pierre Rousselin
2024	—	`conf`	Teaching Divisibility and Binomials with Coq. ThEdu@CADE Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero, Pierre Rousselin
2023	B	`conf`	A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem. FM Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine
2022	J	`jnl`	A Coq Formalization of Lebesgue Integration of Nonnegative Functions. J. Autom. Reason. Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
2022	J	`jnl`	Lebesgue Induction and Tonelli's Theorem in Coq. CoRR Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine
2021	J	`jnl`	A Coq Formalization of Lebesgue Integration of Nonnegative Functions. CoRR Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
2018	B	`conf`	Formal proof of polynomial-time complexity with quasi-interpretations. CPP Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak
2017	B	`conf`	A Coq formal proof of the LaxMilgram theorem. CPP Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
2015	J	`jnl`	Formally Verified Certificate Checkers for Hardest-to-Round Computation. J. Autom. Reason. Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, Laurent Théry
2014	J	`jnl`	Trusting computations: A mechanized proof from partial differential equations to actual program. Comput. Math. Appl. Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2013	Misc	`conf`	Certified, Efficient and Sharp Univariate Taylor Models in COQ. SYNASC Érik Martin-Dorel, Laurence Rideau, Laurent Théry, Micaela Mayero, Ioana Pasca
2013	J	`jnl`	Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. J. Autom. Reason. Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2012	—	`conf`	Rigorous Polynomial Approximation Using Taylor Models in Coq. NASA Formal Methods Nicolas Brisebarre, Mioara Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca, Laurence Rideau, Laurent Théry
2012	J	`jnl`	Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. CoRR Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2011	J	`jnl`	Wave Equation Numerical Resolution: Mathematics and Program CoRR Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2010	J	`jnl`	Coloured Petri net refinement specification and correctness proof with Coq. Innov. Syst. Softw. Eng. Christine Choppy, Micaela Mayero, Laure Petrucci
2010	J	`jnl`	Formal Proof of SCHUR Conjugate Function CoRR Franck Butelle, Florent Hivert, Micaela Mayero, Frédéric Toumazet
2010	—	`conf`	Formal Proof of SCHUR Conjugate Function. AISC/MKM/Calculemus Franck Butelle, Florent Hivert, Micaela Mayero, Frédéric Toumazet
2010	B	`conf`	Formal Proof of a Wave Equation Resolution Scheme: The Method Error. ITP Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2010	J	`jnl`	Formal Proof of a Wave Equation Resolution Scheme: the Method Error CoRR Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2009	—	`conf`	Coloured Petri net refinement specification, and correctness proof with Coq. NASA Formal Methods Christine Choppy, Micaela Mayero, Laure Petrucci
2008	—	`conf`	Experimenting Formal Proofs of Petri Nets Refinements. Refine@FM Christine Choppy, Micaela Mayero, Laure Petrucci
2006	J	`jnl`	The Three Gap Theorem (Steinhauss Conjecture) CoRR Micaela Mayero
2005	J	`jnl`	Dealing with algebraic expressions over a field in Coq using Maple. J. Symb. Comput. David Delahaye, Micaela Mayero
2005	J	`jnl`	Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant CoRR David Delahaye, Micaela Mayero
2005	—	`conf`	Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System. Calculemus David Delahaye, Micaela Mayero
2002	—	`conf`	Using Theorem Proving for Numerical Analysis (Correctness Proof of an Automatic Differentiation Algorithm). TPHOLs Micaela Mayero
2001	—	`conf`	Field, une procédure de décision pour les nombres réels en Coq. JFLA David Delahaye, Micaela Mayero
1999	—	`conf`	The Three Gap Theorem (Steinhaus Conjecture). TYPES Micaela Mayero