A. Asperti, W. Ricciotti, C. Sacerdoti-coen, and E. Tassi, The matita interactive theorem prover, 2011.

A. Bove, P. Dybjer, and U. Norell, A brief overview of agda -a functional language with dependent types, 2009.

F. Baader and T. Nipkow, Term Rewriting and All That, 1999.

D. Cousineau and G. Dowek, Embedding pure type systems in the lambdapi-calculus modulo, TLCA, 2007.

A. Church, A formulation of the simple theory of types, Journal of Symbolic Logic, vol.5, issue.2, pp.56-68, 1940.

F. Durán and H. Garavel, The rewrite engines competitions : A rectrospective, TACAS, 2019.

, Coq development team. The coq proof assistant manual : version 8.9, 2018.

S. Egi, Egison : Non-linear pattern-matching against non-free data types, ArXiv, 2015.

S. Eker, Fast matching in combinations of regular equational theories, First International Workshop on Rewriting Logic and its Applications, vol.4, pp.90-109, 1996.

S. Egi and Y. Nishiwaki, Non-linear pattern matching with backtracking for non-free data types, ArXiv, 2018.

R. Harper, F. Honsell, and G. D. Plotkin, A framework for defining logics, J. ACM, vol.40, pp.143-184, 1987.

A. William, D. Howard-;-xavier-leroy, A. Doligez, J. Frisch, J. Garrigue et al., The ocaml system release 4.06 : Documentation and user's manual, 1969.

R. Lepigre and C. Raffalli, Abstract representation of binders in ocaml using the bindlib library, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01972050

L. Maranget, Compiling pattern matching to good decision trees, 2008.

A. Middeldorp, Term Rewriting, 2019.
URL : https://hal.archives-ouvertes.fr/hal-00338565

D. Miller, A logic programming language with lambda-abstraction, function variables, and simple unification, Extensions of Logic Programming, 1990.

C. Benjamin and . Pierce, Types and Programming Languages, 2002.

C. Lawrence, T. Paulson, and . Nipkow, Isabelle a generic theorem prover, 1994.

H. Kristoffer and . Rose, CRSX -Combinatory Reduction Systems with Extensions, 22nd International Conference on Rewriting Techniques and Applications (RTA'11), vol.10, pp.81-90, 2011.

B. Russell, Mathematical logic as based on the theory of types, American Journal of Mathematics, vol.30, issue.3, pp.222-262, 1908.

R. Saillard, Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. Theses, Ecole Nationale Supérieure des Mines de Paris, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01299180

C. Schürmann, The twelf proof assistant, TPHOLs, 2009.

, There are basic types such as ? bool booleans ? string ? int integers ? float ? unit and type constructor which can be used to build other types, such as list, array, &c. Type constructors are usually used in postfix notation, meaning that the type of a list of integers is noted int list. Such type constructors are said polymorphic, meaning that they can take any type as argument. Arguments of type constructors are usually noted 'a, 'b &c. and read as , &c. We can now mention the essential type constructors

, ? 'a list type of lists. We give some examples of types, (bool * bool) list

, * 'b) list -> 'a -> 'b (** Function searching for a key of type 'a and returning the corresponding element of type

, The infix cons operator :: is of type 'a -> 'a list -> 'a list and puts its left argument on top of its right one. Therefore, A.2.1. Basic values ? Booleans : true and false. ? Integers : 0, 1, ? ? Lists : the empty list