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

A. Bakewell, S. Carlier, A. J. Kfoury, and J. B. Wells, Exact intersection typing inference and call-by-name evaluation, 2004.

A. Bakewell and A. J. Kfoury, Unification with expansion variables, 2004.

H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, 1984.

S. Carlier, J. Polakow, J. B. Wells, and A. J. Kfoury, System??E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types, Programming Languages & Systems, 13th European Symp. Programming, pp.294-309, 2004.
DOI : 10.1007/978-3-540-24725-8_21

S. Carlier and J. B. Wells, Type inference with expansion variables and intersection types in system E and an exact correspondence with ??-reduction, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '04, 2004.
DOI : 10.1145/1013963.1013980

D. D. Champeaux, About the Paterson-Wegman linear unification algorithm, Journal of Computer and System Sciences, vol.32, issue.1, pp.79-90, 1986.
DOI : 10.1016/0022-0000(86)90003-6

A. J. Kfoury, Beta-reduction as unification. A refereed extensively edited version is [9]. This preliminary version was presented at the Helena Rasiowa Memorial Conference, 1996.

A. J. Kfoury, Beta-reduction as unification, Logic, Algebra, and Computer Science (H. Rasiowa Memorial Conference Banach Center Publication, pp.137-158, 1996.

A. J. Kfoury, G. Washburn, and J. B. Wells, Implementing Compositional Analysis Using Intersection Types With Expansion Variables, Proceedings of the 2nd Workshop on Intersection Types and Related Systems The ITRS '02 proceedings appears as, 2002.
DOI : 10.1016/S1571-0661(04)80494-8

A. J. Kfoury and J. B. Wells, Principality and decidable type inference for finite-rank intersection types, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.161-174, 1999.
DOI : 10.1145/292540.292556

A. J. Kfoury and J. B. Wells, Principality and type inference for intersection types using expansion variables, Theoretical Computer Science, vol.311, issue.1-3, 2003.
DOI : 10.1016/j.tcs.2003.10.032

A. J. Kfoury and J. B. Wells, Principality and type inference for intersection types using expansion variables, Theoretical Computer Science, vol.311, issue.1-3, pp.1-3, 2004.
DOI : 10.1016/j.tcs.2003.10.032

M. Paterson and M. Wegman, Linear unification, Journal of Computer and System Sciences, vol.16, issue.2, pp.158-167, 1978.
DOI : 10.1016/0022-0000(78)90043-0

S. Rocca, Principal type scheme and unification for intersection type discipline, Theoretical Computer Science, vol.59, issue.1-2, pp.181-209, 1988.
DOI : 10.1016/0304-3975(88)90101-6

R. Della-rocca and B. Venneri, Principal type schemes for an extended type theory, Theoretical Computer Science, vol.28, issue.1-2, pp.151-169, 1984.
DOI : 10.1016/0304-3975(83)90069-5

S. J. Van-bakel, Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems, 1993.

R. 1. Dauchet and S. Tison, The theory of ground rewrite systems is decidable, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.242-248, 1990.
DOI : 10.1109/LICS.1990.113750

V. Gouranton, P. Réty, and H. Seidl, Synchronized Tree Languages Revisited and New Applications, Proceedings of 6th Conference on Foundations of Software Science and Computation StructuresItaly), 2001.
DOI : 10.1007/3-540-45315-6_14

P. Gyenizse and S. Vagvolgyi, Linear generalized semi-monadic rewrite systems effectively preserve recognizability, Theoretical Computer Science, vol.194, issue.1-2, pp.87-122, 1998.
DOI : 10.1016/S0304-3975(96)00333-7

F. Jacquemard, Decidable approximations of term rewriting systems, Proceedings 7th Conference RTA, pp.362-376, 1996.
DOI : 10.1007/3-540-61464-8_65

S. Limet and P. Réty, E-unification by means of tree tuple synchronized grammars, Discrete Mathematics and Theoritical Computer Science, vol.1, pp.69-98, 1997.
DOI : 10.1007/BFb0030616
URL : https://hal.archives-ouvertes.fr/hal-00809528

S. Limet and G. Salzer, Proving Properties of Term Rewrite Systems via Logic Programs, proceedings of RTA, pp.170-184, 2004.
DOI : 10.1007/978-3-540-25979-4_12

S. Limet and G. Salzer, Manipulating tree tuple languages by transforming logic programs, Electronic Notes in Theoretical Computer Science, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00085313

C. Loding, Model-Checking Infinite Systems Generated by Ground Tree Rewriting, Proceedings of the 7th Conference on Foundations of Software Science and Computation Structures, 2002.
DOI : 10.1007/3-540-45931-6_20

P. Réty, Regular Sets of Descendants for Constructor-Based Rewrite Systems, Proceedings of the 6th international conference LPAR, number 1705 in Lecture Notes in Artificial Intelligence (LNAI), 1999.
DOI : 10.1007/3-540-48242-3_10

P. Réty and J. Vuotto, Context-Free Tree Languages for Descendants, 5th Workshop on Rule-Based Programming Proceedings in ENTCS vol, 2005.
DOI : 10.1016/j.entcs.2004.07.016

H. Seki, T. Takai, F. Youhei, and Y. Kaji, Layered Transducing Term Rewriting System and Its Recognizability Preserving Property, 13th International Conference RTA, volume 2378 of Lectures Notes in computer Science, 2002.
DOI : 10.1007/3-540-45610-4_8

T. Takai, Y. Kaji, and H. Seki, Right-Linear Finite Path Overlapping Term Rewriting Systems Effectively Preserve Recognizability, Proceedings 11th Conference RTA, pp.246-260, 2000.
DOI : 10.1007/10721975_17

R. 1. Armando, S. Ranise, and M. Rusinowitch, Uniform Derivation of Decision Procedures by Superposition, Proceedings 15th Workshop on Computer Science Logic, pp.513-527, 2001.
DOI : 10.1007/3-540-44802-0_36
URL : https://hal.archives-ouvertes.fr/inria-00100412

L. Bachmair and H. Ganzinger, Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, vol.4, issue.3, pp.1-31, 1994.
DOI : 10.1093/logcom/4.3.217

C. Lynch and B. Morawska, Automatic decidability, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp.7-16, 2002.
DOI : 10.1109/LICS.2002.1029813
URL : https://hal.archives-ouvertes.fr/inria-00586936

C. Lynch and B. Morawska, Basic Syntactic Mutation, Proceedings of Conference on Automated Deduction (CADE), pp.471-485, 2002.
DOI : 10.1007/3-540-45620-1_37

S. Mitra, Semantic Unification for Convergent Systems

R. Nieuwenhuis, On narrowing, refutation proofs and constraints, 6th International Conference on Rewriting Techniques and Applications (RTA) Springer- Verlag LNCS 914, pp.56-70, 1995.
DOI : 10.1007/3-540-59200-8_47

R. Nieuwenhuis, Decidability and Complexity Analysis by Basic Paramodulation, Information and Computation, vol.147, issue.1, pp.1-21, 1998.
DOI : 10.1006/inco.1998.2730
URL : http://doi.org/10.1006/inco.1998.2730

C. Weidenbach, Sorted Unification and Tree Automata in Automated Deduction -A Basis for Applications, pp.291-320, 1998.

R. 1. Abadi, B. Blanchet, and C. Fournet, Just Fast Keying in the Pi Calculus, Proceedings of ESOP'04, pp.340-354, 2004.
DOI : 10.1007/978-3-540-24725-8_24

R. Amadio, D. Lugiez, and V. Vanackère, On the symbolic reduction of processes with cryptographic functions, Theoretical Computer Science, vol.290, issue.1, pp.695-740, 2003.
DOI : 10.1016/S0304-3975(02)00090-7
URL : https://hal.archives-ouvertes.fr/inria-00072478

F. Baader and K. U. Schulz, Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures, Journal of Symbolic Computation, vol.21, issue.2, pp.211-243, 1996.
DOI : 10.1006/jsco.1996.0009

D. Basin, S. Mödersheim, and L. Viganò, An On-the-Fly Model-Checker for Security Protocol Analysis, Proceedings of ESORICS'03, pp.253-270, 2003.
DOI : 10.1007/978-3-540-39650-5_15

M. Boreale, Symbolic Trace Analysis of Cryptographic Protocols, Proceedings of the 28th ICALP'01, pp.667-681, 2001.
DOI : 10.1007/3-540-48224-5_55

M. Boreale and M. Buscemi, Symbolic Analysis of Crypto-Protocols Based on Modular Exponentiation, Proceedings of MFCS 2003, 2003.
DOI : 10.1007/978-3-540-45138-9_21

N. Borisov, I. Goldberg, and D. Wagner, Intercepting mobile communications, Proceedings of the 7th annual international conference on Mobile computing and networking , MobiCom '01, pp.180-189, 2001.
DOI : 10.1145/381677.381695

Y. Chevalier, R. Kuesters, M. Rusinowitch, and M. Turuani, An NP decision procedure for protocol insecurity with XOR, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., 2003.
DOI : 10.1109/LICS.2003.1210066
URL : https://hal.archives-ouvertes.fr/inria-00071889

Y. Chevalier and M. Rusinowitch, Combining Intruder Theories, 2005.
DOI : 10.1007/11523468_52
URL : https://hal.archives-ouvertes.fr/inria-00070512

Y. Chevalier and L. Vigneron, A tool for lazy verification of security protocols, Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001), 2001.
DOI : 10.1109/ASE.2001.989832
URL : https://hal.archives-ouvertes.fr/inria-00107545

H. Comon-lundh and V. Shmatikov, Intruder deductions, constraint solving and insecurity decision in presence of exclusive or, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pp.271-280, 2003.
DOI : 10.1109/LICS.2003.1210067

S. Delaune and F. Jacquemard, A decision procedure for the verification of security protocols with explicit destructors, Proceedings of the 11th ACM conference on Computer and communications security , CCS '04, pp.278-287, 2004.
DOI : 10.1145/1030083.1030121
URL : https://hal.archives-ouvertes.fr/inria-00579012

N. Dershowitz and J. Jouannaud, Rewrite Systems, Handbook of Theoretical Computer Science, pp.243-320, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

G. Guo, P. Narendran, and D. A. Wolfram, Unification and matching modulo nilpotence, Information and Computation, issue.12, pp.1623-1646, 2000.
DOI : 10.1007/3-540-61511-3_90

J. Hsiang and M. Rusinowitch, On word problems in equational theories, ICALP, pp.54-71, 1987.
DOI : 10.1007/3-540-18088-5_6
URL : https://hal.archives-ouvertes.fr/inria-00075875

C. Meadows and P. Narendran, A unification algorithm for the group Diffie-Hellman protocol, Workshop on Issues in the Theory of Security (in conjunction with POPL'02), 2002.

J. Millen and V. Shmatikov, Constraint solving for bounded-process cryptographic protocol analysis, Proceedings of the 8th ACM conference on Computer and Communications Security , CCS '01, pp.166-175, 2001.
DOI : 10.1145/501983.502007

J. Millen and V. Shmatikov, Symbolic protocol analysis with an abelian group operator or Diffie-Hellman exponentiation, Journal of Computer Security, 2005.

M. Rusinowitch and M. Turuani, Protocol insecurity with finite number of sessions is NPcomplete, Proc.14th IEEE Computer Security Foundations Workshop, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00100411

M. Schmidt-schauß, Unification in a combination of arbitrary disjoint equational theories, Journal of Symbolic Computation, vol.8, issue.1-2, pp.51-99, 1989.
DOI : 10.1016/S0747-7171(89)80022-7

R. 1. Alpuente, D. Ballis, and M. Falaschi, A Rewriting-based Framework for Web Sites Verification, Electronic Notes in Theoretical Computer Science, vol.124, issue.1, 2004.
DOI : 10.1016/j.entcs.2004.07.014

H. Boley, A Tight, Practical Integration of Relations and Functions, volume 1712 of LNAI, 1999.

A. Bonifati and S. Ceri, Comparative analysis of five XML query languages, ACM SIGMOD Record, vol.29, issue.1, pp.68-79, 2000.
DOI : 10.1145/344788.344822

F. Bry and S. Schaffert, Towards a Declarative Query and Transformation Language for XML and Semistructured Data: Simulation Unification, Proc. of International Conference on Logic Programming (ICLP), number 2401, 2002.
DOI : 10.1007/3-540-45619-8_18

B. Buchberger and A. Cr?aciuncr?aciun, Algorithm Synthesis by Lazy Thinking: Examples and Implementation in Theorema, Proc. of the Mathematical Knowledge Management Symposium, pp.24-59, 2003.
DOI : 10.1016/j.entcs.2003.12.027

B. Buchberger, C. Dupré, T. Jebelean, F. Kriftner, K. Nakagawa et al., The Theorema project: A progress report, Proc. of Calculemus'2000 Conference, pp.98-113, 2000.

J. Coelho and M. Florido, CLP(Flex): Constraint Logic Programming Applied to XML Processing, On the Move to Meaningful Internet Systems 2004: CoopIS, DOA, and ODBASE. Proc. of Confederated Int. Conferences, pp.1098-1112, 2004.
DOI : 10.1007/978-3-540-30469-2_17

H. Comon, Completion of Rewrite Systems with Membership Constraints Part I: Deduction Rules, Journal of Symbolic Computation, vol.25, issue.4, pp.397-419, 1998.
DOI : 10.1006/jsco.1997.0185

H. Comon, Completion of Rewrite Systems with Membership Constraints Part II: Constraint Solving, Journal of Symbolic Computation, vol.25, issue.4, pp.421-453, 1998.
DOI : 10.1006/jsco.1997.0186

T. Furche, F. Bry, S. Schaffert, R. Orsini, I. Horroks et al., Survey over existing query and transformation languages Available from: http://rewerse, 2004.

M. L. Ginsberg, The MVL theorem proving system, ACM SIGART Bulletin, vol.2, issue.3, pp.57-60, 1991.
DOI : 10.1145/122296.122304

M. Hamana, Term rewriting with sequences, Proc. of the First Int. Theorema Workshop, 1997.

M. R. Henzinger, T. A. Henzinger, and P. W. Kopke, Computing simulations on finite and infinite graphs, Proceedings of IEEE 36th Annual Foundations of Computer Science, pp.453-462, 1995.
DOI : 10.1109/SFCS.1995.492576

H. Hosoya and B. Pierce, Regular expression pattern matching for XML, Journal of Functional Programming, vol.13, issue.6, pp.961-1004, 2003.
DOI : 10.1017/S0956796802004410

T. Kutsia, Solving and Proving in Equational Theories with Sequence Variables and Flexible Arity Symbols, 2002.

T. Kutsia, Unification with Sequence Variables and Flexible Arity Symbols and Its Extension with Pattern-Terms, Artificial Intelligence, Automated Reasoning and Symbolic Computation. Proc. of Joint AISC'2002 ? Calculemus'2002 Conference, volume 2385 of LNAI, pp.290-304, 2002.
DOI : 10.1007/3-540-45470-5_26

T. Kutsia, Solving Equations Involving Sequence Variables and Sequence Functions, Artificial Intelligence and Symbolic Computation . Proc. of AISC'04 Conference, pp.157-170, 2004.
DOI : 10.1007/978-3-540-30210-0_14

T. Kutsia, Context Sequence Matching for XML, Proc. of First International Workshop on Automated Specification and Verification of Web Sites (WWV'05), pp.103-119, 2005.
DOI : 10.1016/j.entcs.2005.12.045
URL : http://doi.org/10.1016/j.entcs.2005.12.045

J. Levy and M. Villaret, Linear second-order unification and context unification with treeregular constraints, Proc. of the 11th Int. Conference on Rewriting Techniques and Applications (RTA'2000), volume 1833 of LNCS, pp.156-171, 2000.

D. Maier, Database desiderata for an XML query language Available from: http: //www.w3.org/TandS, 1998.

M. Marin and D. , Package, Challenging the Boundaries of Symbolic Computation, pp.17-24, 2003.
DOI : 10.1142/9781848161313_0003
URL : https://hal.archives-ouvertes.fr/hal-01357765

S. Anantharaman, P. Narendran, and M. Rusinowitch, ACID-Unification Is NEXPTIME-Decidable, Proc. of MFCS'03, pp.169-179, 2003.
DOI : 10.1007/978-3-540-45138-9_11
URL : https://hal.archives-ouvertes.fr/hal-00080663

S. Anantharaman, P. Narendran, and M. Rusinowitch, Unification Modulo ACUI Plus Distributivity Axioms, Journal of Automated Reasoning, vol.3, issue.1?2, pp.1-28, 2004.
DOI : 10.1007/s10817-004-2279-7
URL : https://hal.archives-ouvertes.fr/inria-00099990

S. Anantharaman, P. Narendran, and M. Rusinowitch, Closure Properties and Decision Problems of Dag Automata Information Processing Letters, 2005.

F. Baader and P. Narendran, Unification of Concept Terms in Description Logics, Journal of Symbolic Computation, vol.31, issue.3, pp.277-305, 2001.
DOI : 10.1006/jsco.2000.0426

P. Buneman, M. Grohe, and C. Koch, Path Queries on Compressed XML, Proc. of the 29th Conf. on VLDB, pp.141-152, 2003.
DOI : 10.1016/B978-012722442-8/50021-5

W. Charatonik, Automata on DAG Representations of Finite Trees

T. Genet and F. Klay, Rewriting for Cryptographic Protocol Verification, Proc. of the 17th CADE, pp.271-290, 1831.
DOI : 10.1007/10721959_21
URL : https://hal.archives-ouvertes.fr/inria-00072731

R. Gilleron, S. Tison, and M. Tommasi, Set Constraints and Automata, Information and Computation, vol.149, issue.1, pp.1-41, 1996.
DOI : 10.1006/inco.1998.2747
URL : https://hal.archives-ouvertes.fr/inria-00538886

M. Frick, M. Grohe, and C. Koch, Query evaluation on compressed trees, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pp.188-197
DOI : 10.1109/LICS.2003.1210058

M. Marx, XPath and Modal Logics for Finite DAGs, Proc. of TABLEAUX'03, pp.150-164, 2003.

M. Minsky, Computation: Finite and Infinite Machines, 1972.

F. Neven, A. Theory, . Xml-researchers, G. Sigmo-record, T. Dowek et al., References 1 Unification via explicit substitutions: The case of higher-order patterns, 1998.

M. P. Fiore, G. D. Plotkin, and D. Turi, Abstract syntax and variable binding, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.193-202, 1999.
DOI : 10.1109/LICS.1999.782615

M. J. Gabbay and A. M. Pitts, A New Approach to Abstract Syntax with Variable Binding, Formal Aspects of Computing, vol.13, issue.3-5, pp.341-363, 2002.
DOI : 10.1007/s001650200016

M. Hamana, A Logic Programming Language Based on Binding Algebras, Proc. Theoretical Aspects of Computer Science number 2215 in Lecture Notes in Computer Science, pp.243-262, 2001.
DOI : 10.1007/3-540-45500-0_12

M. Hamana, Simple ?0-unification for terms with context holes, Proceedings of the 16th International Workshop on Unification, pp.9-13, 2002.

G. Huet, A unification algorithm for typed ??-calculus, Theoretical Computer Science, vol.1, issue.1, pp.27-67, 1975.
DOI : 10.1016/0304-3975(75)90011-0

D. Miller, A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification, Journal of Logic and Computation, vol.1, issue.4, pp.497-536, 1991.
DOI : 10.1093/logcom/1.4.497

D. Miller, Unification of simply typed lambda-terms as logic programming, Logic Programming, Proceedings of the Eighth International Conference, pp.255-269, 1991.

D. Miller, Unification under a mixed prefix, Journal of Symbolic Computation, vol.14, issue.4, pp.321-358, 1992.
DOI : 10.1016/0747-7171(92)90011-R

D. Miller and A. Tiu, A proof theory for generic judgments: an extended abstract, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pp.118-127, 2003.
DOI : 10.1109/LICS.2003.1210051

T. Nipkow, Functional unification of higher-order patterns, [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp.64-74, 1993.
DOI : 10.1109/LICS.1993.287599

A. M. Pitts and M. J. Gabbay, A Metalanguage for Programming with Bound Names Modulo Renaming, Proc. 5th Int. Conf. on Mathematics of Programme Construction (MPC2000), number 1837 in Lecture Notes in Computer Science, pp.230-255, 2000.
DOI : 10.1007/10722010_15

Z. Qian, Linear unification of higher-order patterns, Proceedings of the International Joint Conference CAAP/FASE on Theory and Practice of Software Development, pp.391-405, 1993.
DOI : 10.1007/3-540-56610-4_78

M. R. Shinwell, A. M. Pitts, and M. J. Gabbay, FreshML: Programmming with binders made simple, Proc. 8th ACM SIGPLAN Int. Conf. on Functional Programming, pp.263-274, 2003.

C. Urban, A. M. Pitts, and M. J. Gabbay, Nominal unification following, we denote the transformation using a rule " rule " by " ? rule " . Rules for second-order matching: E=E ? ? {s, t}, s=@(s r ), Theoretical Computer Science, vol.323, pp.1-3473, 2004.

?. Simp, Simplification rule): (1) If s = t and s ? IC or s = w: E=E ? ? {s, t} ? Simp E ? (2) If hd(s) = hd(t)

E. {?, ?. Simp, and E. {?, ? Simp E ? ? {s 1 , t 1 , · · · , s m , t m } (3) If s = Qx.?, t = Qy.?, Imitation rule): (1) If t=Qx.?(t d ) (Q ? {?, ?}) and ? (s)=? (Qx.?(t d ))=o: E ? Imit E[@ := ?v r .Qx.?(H 1 (x, v r ), . . . , H d (x

. Proj, Projection rule), where ¯ s r = (s 1 , . . . , s r )

B. Brock, S. Cooper, and W. Pierce, Analogical reasoning and proof discovery, LNCS, issue.310, pp.454-468, 1988.
DOI : 10.1007/BFb0012849

R. Curien, Z. Qian, and H. Shi, Efficient second-order matching, RTA 96(Rewriting Techniques and Application), pp.317-331, 1996.
DOI : 10.1007/3-540-61464-8_62

M. R. Donat and L. A. Wallen, Learning and applying generalised sotutions using higher order resolution, LNCS, issue.310, pp.41-60, 1988.

G. Dowek, Third order matching is decidable, 7th Annual IEEE Symposium on Logic in Computer Science, pp.2-10, 1992.
DOI : 10.1016/0168-0072(94)90083-3

P. Flener, Logic program synthesis from incomplete information, 1995.
DOI : 10.1007/978-1-4615-2205-8

M. Harao, Proof discovery in LK system by analogy, LNCS(Proc. of the 3rd Asian Computing Science Conference), pp.197-211, 1997.
DOI : 10.1007/3-540-63875-X_53

M. Harao and K. Iwanuma, Complexity of higher-order unification algorithm. Society for Software Science and Technology, pp.41-53, 1991.

M. Harao, K. Yamada, and K. Hirata, Efficient second order predicate matching algorithm, Proc. Korea-Japan Joint Workshop on Algorithm and Computations, pp.31-39, 1999.

K. Hirata, K. Yamada, and M. Harao, Tractable and intractable second-order matching problems, Journal of Symbolic Computation, vol.37, issue.5, pp.611-628, 2004.
DOI : 10.1016/j.jsc.2003.09.002

G. P. Huet, A unification algorithm for typed ??-calculus, Theoretical Computer Science, vol.1, issue.1, pp.27-57, 1975.
DOI : 10.1016/0304-3975(75)90011-0

G. P. Huet and B. Lang, Proving and applying program transformations expressed with second-order patterns, Acta Informatica, vol.11, issue.1, pp.31-55, 1978.
DOI : 10.1007/BF00264598

P. Kilpeläinen, Tree Matching Problems with Applications to Structured Text Databases, 1992.

D. A. Miller, A logic programming language with lambda-abstraction function variables, and simple unification, J. of Logic and Computations, vol.1, issue.4, pp.494-536, 1991.

A. S. Troelstra and H. Schwichtenberg, Basic proof Theory, 1996.
DOI : 10.1017/CBO9781139168717

K. Yamada, K. Hirata, and M. Harao, Schema matching and its complexity J82-D-I, Trans. IEICE, pp.1307-1316, 1999.

K. Yamada, S. Yin, M. Harao, and K. Hirata, Development of an analogy-based generic sequent style automatic theorem prover amalgamated with interactive proving, Proc. of IWIL'05 (the International Workshop on the Implementation of Logics 2005), 2005.

R. 1. Futatsugi, J. A. Goguen, J. P. Jouannaud, and J. Meseguer, Principles of OBJ2, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '85, pp.52-66, 1985.
DOI : 10.1145/318593.318610