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

Finite Groups Representation Theory with Coq. - Sidi Ould Biha (Calculemus/MKM, 2009)

Composants mathématiques pour la théorie des groupes. (Mathematical components for groups theory). - Sidi Ould Biha (2010)

A Formal Semantics of PLC Programs in Coq. - Sidi Ould Biha (COMPSAC, 2011)

Verification of PLC Properties Based on Formal Semantics in Coq. - Jan Olaf Blech; Sidi Ould Biha (SEFM, 2011)

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)

On Formal Reasoning on the Semantics of PLC using Coq - Jan Olaf Blech; Sidi Ould Biha (CoRR, 2013)