A. Team, The Asf+Sdf Meta-Environment Home Page'. http://www.cwi.nl/ htbin/sen1, 2005.

G. Barthe, Pure Pattern Type Systems, Proc. of POPL, 2003.

&. P. Boudol and . Zimmer, Recursion in the Call-by-Value Lambda-Calculus, Proc. of FICS, Note Series NS-02-2. BRICS, 2002.

H. Cirstea and &. C. Kirchner, The rewriting calculus - part II, Logic Journal of IGPL, vol.9, issue.3, pp.427-498, 2001.
DOI : 10.1093/jigpal/9.3.377
URL : https://hal.archives-ouvertes.fr/inria-00100532

H. Cirstea, Matching Power, Proc. of RTA, pp.77-92, 2001.
DOI : 10.1007/3-540-45127-7_8
URL : https://hal.archives-ouvertes.fr/inria-00099308

H. Cirstea, The Rho Cube, Proc. of FOSSACS, pp.166-180, 2001.
DOI : 10.1007/3-540-45315-6_11
URL : https://hal.archives-ouvertes.fr/inria-00107877

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

H. Cirstea, Rho-calculus with Fixpoint: First-order system, Proc. of TYPES, 2004.

G. Cousineau, The categorical abstract machine, Science of Computer Programming, vol.8, issue.2, pp.173-202, 1987.
DOI : 10.1016/0167-6423(87)90020-7

. Cristal, Concert: Compilateurs Certifiés'. ARC INRIA, 2003.

&. P. Faure and . Moreau, Jrho: a Java Implementation of the Rho Calculus, 2002.

M. Felleisen and &. D. Friedman, A syntactic theory of sequential state, Theoretical Computer Science, vol.69, issue.3, pp.243-287, 1989.
DOI : 10.1016/0304-3975(89)90069-8

A. Frisch, The Cduce Home Page, 2005.

E. Gamma, Design Patterns Elements of Reusable Object-Oriented Software, 1994.

E. Gimenez, Structural recursive definitions in type theory, Proc. of ICALP, pp.397-408, 1998.
DOI : 10.1007/BFb0055070

J. Goguen, The OBJ Family Home Page, 2005.

M. Hanus, A unified computation model for functional and logic programming, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.80-93, 1997.
DOI : 10.1145/263699.263710

T. Hirschowitz, Compilation of extended recursion in call-by-value functional languages, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming , PPDP '03, 2003.
DOI : 10.1145/888251.888267
URL : https://hal.archives-ouvertes.fr/hal-00310121

G. Huet, Résolution d'equations dans les langages d'ordre 1, 1976.

S. P. Jones, Haskell 98 Language and Libraries, The Journal of Functional Programming, 2003.

G. Kahn, Natural semantics, Proc. of STACS, pp.22-39, 1987.
DOI : 10.1007/BFb0039592
URL : https://hal.archives-ouvertes.fr/inria-00075953

J. Klop, Combinatory Reduction Systems, 1980.

. Kowalski, Logic for problem solving, ACM SIGSOFT Software Engineering Notes, vol.7, issue.2, 1979.
DOI : 10.1145/1005937.1005947

P. J. Landin, The Mechanical Evaluation of Expressions, The Computer Journal, vol.6, issue.4, pp.308-320, 1964.
DOI : 10.1093/comjnl/6.4.308

K. Lee, HydroJ: Object-Oriented Pattern Matching for Evolvable Distributed Systems, Proc. of OOPSLA, 2003.

X. Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00000963

&. B. Liquori and . Serpette, Web Appendix of this paper'. http://www-sop.inria.fr/ mascotte/Luigi.Liquori/iRhoThe Coq Home Page, Logical Team, 2005.

P. Martin-löf, Intuitionistic Type Theory of Studies in Proof Theory, 1984.

I. A. Mason and &. L. Talcott, References, local variables and operational reasoning, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pp.66-77, 1992.
DOI : 10.1109/LICS.1992.185532
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.1123

M. Team, The Maude Home Page, 2005.

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

N. P. Mendler, Infinite Objects in Type Theory, Proc. of LICS, pp.249-255, 1986.

. Microsoft, The C# Home Page, 2005.

R. Milner and R. Milner, 'CS 3 Language Semantics'. Course notes The Definition of Standard ML (Revised), 1986.

. Moreau, The Tom Home Page, 2003.

J. G. Morrisett, Abstract models of memory management, Proceedings of the seventh international conference on Functional programming languages and computer architecture , FPCA '95, pp.66-77, 1995.
DOI : 10.1145/224164.224182

G. D. Plotkin, A Structured Approach to Operational Semantics, 1981.

G. D. Plotkin, The Origins of Structural Operational Semantics, J. Log. Algebr. Program, pp.60-613, 2004.

J. R. Kelsey and W. Clinger, Revised5 Report on the Algorithmic Language Scheme, Higher-Order and Symbolic Computation, 1998.

&. H. Riehle and . Züllighoven, Understanding and using patterns in software development, Theory and Practice of Object Systems, pp.3-13, 1996.
DOI : 10.1002/(SICI)1096-9942(1996)2:1<3::AID-TAPO1>3.0.CO;2-#

M. Serrano, The Scheme Bigloo Home Page, 2005.

S. Team, The Rho Stratego Home Page'. http://www.stratego-language.org/ twiki, 2003.

S. Team, The Stratego Home Page, 2005.

A. Stump, CVC: A Cooperating Validity CheckerThe Rogue Home Page, 2002.

M. Tofte, Operational Semantics and Polymorphic Type Inference, 1987.

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