J. Avenhaus and C. , Loría-Sáenz ? " Higher Order Conditional Rewriting and Narrowing, Proceedings of the 1st International Conference on Constraints in Computational Logics, pp.269-284, 1994.

G. Barthe, H. Cirstea, C. Kirchner, L. Liquori, and ?. , Pure Patterns Type Systems, Principles of Programming Languages, 2003.
DOI : 10.1145/640128.604152
URL : https://hal.archives-ouvertes.fr/inria-00099463

F. Barbanera, M. Fernández, and H. Geuvers, Modularity of strong normalization in the algebraic-??-cube, Journal of Functional Programming, vol.7, issue.6, pp.613-660, 1997.
DOI : 10.1017/S095679689700289X

J. A. Bergstra and J. W. Klop, Conditional rewrite rules: Confluence and termination, Journal of Computer and System Sciences, vol.32, issue.3, pp.323-362, 1986.
DOI : 10.1016/0022-0000(86)90033-4

F. Blanqui, C. Kirchner, C. Riba, and ?. , On the confluence of lambda-calculus with conditional rewriting, Proceedings of FoSSaCS'06Bla05] F. Blanqui ? " Definitions by Rewriting in the Calculus of Constructions, pp.28-37, 2005.
DOI : 10.1016/j.tcs.2009.07.058
URL : https://hal.archives-ouvertes.fr/inria-00000729

V. Breazu-tannen, J. Gallier, and ?. , Polymorphic rewriting conserves algebraic strong normalization and confluence, Proceedings of ICALP'89, p.16, 1989.
DOI : 10.1007/BFb0035757

V. Breazu-tannen, A. Meyer, and ?. , Computable values can be classical, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '87, p.15, 1987.
DOI : 10.1145/41625.41646

H. Cirstea, C. Kirchner, and ?. , 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

D. G. Dowek, T. Hardin, C. Kirchner, and ?. , Theorem Proving Modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506

N. Dershowitz, J. Jouannaud, and ?. , Rewrite Systems Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) (J. van Leeuwen, pp.243-320, 1990.

N. Dershowitz and M. Okada, A rationale for conditional equational programming, Theoretical Computer Science, vol.75, issue.1-2, pp.111-138, 1990.
DOI : 10.1016/0304-3975(90)90064-O

]. D. Dou92 and . Dougherty, Adding Algebraic Rewriting to the Untyped Lambda Calculus, Information and Computation, vol.101, issue.22, pp.251-267, 1992.

J. Glauert, D. Kesner, and Z. Khasidashvili, Expression Reduction Systems and Extensions: An Overview, Processes, Terms and Cycles: Steps to the Road of Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion os His 60th Birthday, pp.496-553, 2005.
DOI : 10.1007/11601548_22
URL : https://hal.archives-ouvertes.fr/hal-00148530

E. Giovannetti, C. Moiso, and ?. , Notes on the Elimination of Conditions On Termination and Confluence Properties of Disjoint and Constructor-Sharing Conditional Rewrite Systems, Proceedings of CTRS'87, pp.91-97, 1988.

G. Huet and ?. , Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM, vol.27, issue.4, pp.797-821, 1980.
DOI : 10.1145/322217.322230

J. Jouannaud, M. Okada, and ?. , Executable Higher-Order Algebraic Specification Languages, Proceedings of LiCS'91, 1991.

]. S. Kap84 and ?. Kaplan, Conditional Rewrite Rules, Theoretical Computer Science, vol.33, pp.175-193, 1984.

J. W. Klop, V. Van-oostrom, and F. Van-raamsdonk, Combinatory reduction systems: introduction and survey, Theoretical Computer Science, vol.121, issue.1-2, pp.279-308, 1993.
DOI : 10.1016/0304-3975(93)90091-7

U. Kühler and C. Wirth, Conditional equational specifications of data types with partial operations for inductive theorem proving, Proceedings of RTA'97Mid91] A. Middeldorp ? " Confluence of the Disjoint Union of Conditional Term Rewriting Systems Proceedings of CTRS'91, pp.38-52, 1991.
DOI : 10.1007/3-540-62950-5_60

F. [. Van-oostrom and . Van-raamsdonk, Weak orthogonality implies confluence: The higher-order case, Proceedings of LFCS'94, p.27, 1920.
DOI : 10.1007/3-540-58140-5_35

M. Parigot and ?. , On the representation of data in lambda-calculus, Proceedings of CSL'89, pp.309-321, 1989.
DOI : 10.1007/3-540-52753-2_47

C. P. Wadsworth, Semantics and Pragmatics of the Lambda-Calculus, Thèse, 1971.