An explicit Eta rewrite rule. - Daniel Briaud (TLCA, 1995)

lambda-nu, A Calculus of Explicit Substitutions which Preserves Strong Normalisation. - Zine-El-Abidine Benaissa; Daniel Briaud; Pierre Lescanne; Jocelyne Rouyer-Degli (J. Funct. Program., 1996)

Substitutions explicites et unification d'ordre supérieur. - Daniel Briaud (1997)