Formalization of a lamda-Calculus with Explicit Substitutions in Coq. - Amokrane Saïbi (TYPES, 1994)

Typing Algorithm in Type Theory with Inheritance. - Amokrane Saïbi (POPL, 1997)

Outils Génériques de Modélisation et de Démonstration pour la Formalisation des Mathématiques en Théorie des Types. Application à la Théorie des Catégories. (Formalization of Mathematics in Type Theory. Generic tools of Modelisation and Demonstration. Application to Category Theory). - Amokrane Saïbi (1999)

Constructive category theory. - Gérard P. Huet; Amokrane Saïbi (Proof, Language, and Interaction, 2000)