Proofs in the Final Algebra. - Laurence Puel (CAAP, 1984)

Embedding with Patterns and Associated Recursive Path Ordering. - Laurence Puel (RTA, 1989)

Using Unavoidable Set of Trees to Generalize Kruskal's Theorem. - Laurence Puel (J. Symb. Comput., 1989)

Extension of the Associative Path Ordering to a Chain of Associative Commutative Symbols. - Catherine Delor; Laurence Puel (RTA, 1993)

Optimal Solutions to Pattern Matching Problems. - Laurence Puel; Ascánder Suárez (TAPSOFT, 1993)

Compiling Pattern Matching by Term Decomposition. - Laurence Puel; Ascánder Suárez (J. Symb. Comput., 1993)

Lambda-Calculi with Explicit Substitutions and Composition Which Preserve Beta-Strong Normalization. - Maria C. F. Ferreira; Delia Kesner; Laurence Puel (ALP, 1996)

A Typed Pattern Calculus. - Delia Kesner; Laurence Puel; Val Tannen (Inf. Comput., 1996)

Reducing AC-Termination to Termination. - Maria C. F. Ferreira; Delia Kesner; Laurence Puel (MFCS, 1998)

lambda-Calculi with Explicit Substitutions Preserving Strong Normalization. - Maria C. F. Ferreira; Delia Kesner; Laurence Puel (Appl. Algebra Eng. Commun. Comput., 1999)