H. Barendregt, Lambda Calculus: its Syntax and Semantics, 1984.

]. H. Bar92 and . Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, pp.118-310, 1992.

G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori, Pure Patterns Type Systems, Proc. of POPL, pp.250-261, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099463

F. [. Clavel, N. Durán, and . Martí-oliet, Polytypic Programming in Maude, Proc. of WRLA. ENTCS, 2000.
DOI : 10.1016/S1571-0661(05)80135-5

]. H. Cir00 and . Cirstea, Rewriting Calculus: Foundations and Applications, 2000.

]. H. Ckl01a, C. Cirstea, L. Kirchner, and . Liquori, Matching Power, Proc. of RTA, pp.77-92, 2001.

]. H. Ckl01b, C. Cirstea, L. Kirchner, and . Liquori, The Rho Cube, Proc. of FOSSACS, pp.166-180, 2001.

H. Cirstea, C. Kirchner, and L. Liquori, Rewriting Calculus with(out) Types, Proc. of WRLA, 2002.
DOI : 10.1016/S1571-0661(05)82526-5
URL : https://hal.archives-ouvertes.fr/inria-00100858

C. [. Cirstea, L. Kirchner, B. Liquori, and . Wack, The Rho Cube, Proc. of HOR, 2002.
DOI : 10.1007/3-540-45315-6_11
URL : https://hal.archives-ouvertes.fr/inria-00107877

L. [. Cirstea, B. Liquori, and . Wack, Rho-calculus with Fixpoint: Firstorder System, Proc. of TYPES, 2004.

M. Clavel and J. Meseguer, Reflection in conditional rewriting logic, Theoretical Computer Science, vol.285, issue.2, pp.245-288, 2002.
DOI : 10.1016/S0304-3975(01)00360-7

]. H. Cur34 and . Curry, Functionality in Combinatory Logic, Proc. Nat. Acad. Sci. U.S.A, pp.584-590, 1934.

L. Damas and R. Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '82, pp.207-212, 1982.
DOI : 10.1145/582153.582176

F. Durán and J. Meseguer, Parameterized Theories and Views in Full Maude 2.0, Proc. of WRLA. ENTCS, 2000.

K. Futatsugi and A. Nakagawa, An Overview of Cafe Project, Proc. of CafeOBJ Workshop, 1996.

F. [. Giannini, S. Honsell, and . Ronchi-della-rocca, Type Inference: Some Results, Some Problems, Fundamenta Informaticae, vol.19, issue.12, pp.87-126, 1993.

J. Y. Girard, The system F of variable types, fifteen years later, Theoretical Computer Science, vol.45, pp.159-192, 1986.
DOI : 10.1016/0304-3975(86)90044-7

]. J. Gog04 and . Goguen, The OBJ Family Home Page, 2004.

S. [. Giannini and . Ronchi-della-rocca, Characterization of typings in polymorphic type discipline, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, pp.61-70, 1988.
DOI : 10.1109/LICS.1988.5101

]. W. How80 and . Howard, The formulas?as?types notion of construction, Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp.479-490, 1980.

]. D. Lei83 and . Leivant, Polymorphic Type Inference, Proc. of POPL, pp.88-98, 1983.

]. L. Liq96 and . Liquori, Type Assigment Systems for Lambda Calculi and for the Lambda Calculus of Objects, 1996.

N. P. Mendler, Inductive Definition in Type Theory, 1987.

J. Meseguer, Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, vol.96, issue.1, pp.73-155, 1992.
DOI : 10.1016/0304-3975(92)90182-F

[. and J. Meseguer, Rewriting Logic: Roadmap and Bibliography, Theoretical Computer Science, vol.285, issue.2, pp.121-154, 2002.

[. Milner, M. Tofte, R. Harper, and D. Macqueen, The Definition of Standard ML (Revised), 1997.

S. and P. Jones, The Implementation of Functional Programming Languages, 1987.

M. Stehr, Programming, Specification and Interactive Theorem Proving ? Towards a Unified Language based on Equational Logic, Rewriting Logic and Type Theory, 2002.

V. Van-oostrom, Lambda Calculus with Patterns, 1990.

J. B. Wells, Typability and type checking in System F are equivalent and undecidable, Annals of Pure and Applied Logic, vol.98, issue.1-3, pp.1-3111, 1999.
DOI : 10.1016/S0168-0072(98)00047-5