Canonical Big Operators. - Yves Bertot; Georges Gonthier; Sidi Ould Biha; Ioana Pasca (TPHOLs, 2008)

Formal Verification of Exact Computations Using Newton's Method. - Nicolas Julien; Ioana Pasca (TPHOLs, 2009)

Formally Verified Conditions for Regularity of Interval Matrices. - Ioana Pasca (AISC/MKM/Calculemus, 2010)

Formal Verifcation for Numerical Methods. (Vérification formelle pour les méthodes numériques). - Ioana Pasca (2010)

Formal proofs for theoretical properties of Newton's method. - Ioana Pasca (Math. Struct. Comput. Sci., 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)

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 001; Assia Mahboubi; Russell O'Connor; Sidi Ould Biha; Ioana Pasca; Laurence Rideau; et al. (ITP, 2013)

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