D. Benanav, D. Kapur, and P. Narendran, Complexity of matching problems, Journal of Symbolic Computation, vol.3, issue.1-2, pp.203-216, 1987.
DOI : 10.1016/S0747-7171(87)80027-5

P. Bendix and D. Knuth, Computational problems in abstract algebra, chapter Simple word problems in universal algebra, 1970.

F. Burton and R. Cameron, Abstract, Journal of Functional Programming, vol.27, issue.02, pp.171-190, 1993.
DOI : 10.1016/0167-6423(90)90070-T

W. Burton, E. Meijer, P. Sansom, S. Thompson, and P. Wadler, Views: An extension to Haskell pattern matching, 1996.

P. and L. Chenadec, Canonical forms in finitely presented algebras. Research notes in theoretical computer science, 1986.

E. Contejean, C. Marché, B. Monate, and X. Urbain, CiME version 2.02. LRI, CNRS UMR 8623, 2004.

C. Development and T. , The Coq Proof Assistant Reference Manual, Version 8.0, 2006.

N. Dershowitz and J. Jouannaud, Rewrite Systems, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

D. Doligez, Zenon, version 0.4.1. http://focal.inria.fr/zenon, 2006.

D. Doligez, J. Garrigue, X. Leroy, D. Rmy, and J. Vouillon, The Objective Caml system release 3.09, Documentation and user's manual, 2005.

J. Gaillourdet, T. Hillenbrand, B. Lchner, and H. Spies, The New WALDMEISTER Loop at Work, Proc. of CADE'03
DOI : 10.1007/978-3-540-45085-6_27

J. Hullot, Compilation de formes canoniques dans les thories quationnelles, 1980.

J. Jouannaud, Modular Church-Rosser Modulo, Proc. of RTA'06
DOI : 10.1007/11805618_8

URL : https://hal.archives-ouvertes.fr/inria-00350970

P. Moreau, C. Ringeissen, and M. Vittek, A pattern matching compiler for multiple target languages, Proc. of CC'03
URL : https://hal.archives-ouvertes.fr/inria-00099427

C. Okasaki, Views for standard ML, Proc. of ML'98

G. Peterson and M. Stickel, Complete Sets of Reductions for Some Equational Theories, Journal of the ACM, vol.28, issue.2, pp.233-264, 1981.
DOI : 10.1145/322248.322251

K. Rao, Completeness of hierarchical combinations of term rewriting systems, Proc. of FSTTCS'93
DOI : 10.1007/3-540-57529-4_48

R. Rioboo, D. Doligez, and T. Hardin, FoCal Reference Manual, version 0.3.1, 2005.

S. Thompson, Laws in Miranda, Proceedings of the 1986 ACM conference on LISP and functional programming , LFP '86
DOI : 10.1145/319838.319839

S. Thompson, Lawful functions and program verification in Miranda, Science of Computer Programming, vol.13, issue.2-3, pp.181-218, 1990.
DOI : 10.1016/0167-6423(90)90070-T

P. Wadler, Views: a way for pattern matching to cohabit with data abstraction, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '87
DOI : 10.1145/41625.41653

P. Weis, Private constructors in OCaml, 2003.