@inproceedings{Cel:97,
  author = {Iliano Cervesato and Frank Pfenning},
  title = {Linear Higher-Order Pre-Unification},
  booktitle = {Proceedings of the Twelfth Annual Sumposium on Logic in Computer Science (LICS'97)},
  publisher = {IEEE Computer Society Press},
  year = {1997},
  pages = {422--433},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.4249Electronic Edition}
}

@inproceedings{DM:04,
  author = {D. Dougherty and C. Martínez},
  title = {Unification and Matching Modulo Type Isomorphism},
  booktitle = {Proceedings of II International Workshop of Higher Order Rewriting},
  year = {2004},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.8353Electronic Edition},
  doi = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.8353}
}

@article{Dow:01,
  author = {G. Dowek},
  title = {Higher-Order Unification and Matching},
  booktitle = {Handbook of Automated Reasoning},
  journal = {Handbook of automated reasoning},
  publisher = {Elsevier Science},
  year = {2001},
  volume = {II},
  pages = {1009--1062},
  note = {http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=778525Electronic Edition},
  url = {http://www.lix.polytechnique.fr/~dowek/Publi/unification.ps}
}

@inproceedings{CE:89,
  author = {Conal Elliott},
  title = {Higher-order Unification with Dependent Function Types},
  booktitle = {RTA},
  year = {1989},
  pages = {121-136}
}

@phdthesis{Eli:90,
  author = {C. M. Elliott},
  title = {Extensions and Applications of Higher-Order Unification},
  school = {School of Computer Science, Carnegie Mellon University},
  year = {1990},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.73.5040Electronic Edition}
}

@article{Far:91,
  author = {W. Farmer},
  title = {Simple second-order languages for which unification is undecidable},
  journal = {Theoretical Computer Science},
  year = {1991},
  volume = {87},
  number = {1},
  pages = {25--41},
  note = {http://dx.doi.org/10.1016/0304-3975(91)90024-VElectronic Edition},
  doi = {http://dx.doi.org/10.1016/0304-3975(91)90024-V}
}

@article{Far:88,
  author = {W. Farmer},
  title = {A Unification Algorithm for Second Order Monadic Terms},
  journal = {Annals of Pure and Applied Logic},
  year = {1988},
  volume = {39},
  pages = {131--174},
  note = {http://dx.doi.org/10.1016/0168-0072(88)90015-2Electronic Edition},
  doi = {http://dx.doi.org/10.1016/0168-0072(88)90015-2}
}

@article{RFBL:96,
  author = {R. Fettig and B. Loechner},
  title = {Unification of Higher-Order Patterns in a Simply Typed Lambda-Calculus with Finite Products and Terminal Type},
  journal = {Lecture Notes in Computer Science},
  year = {1996},
  volume = {1103},
  pages = {347--??}
}

@article{Gol:81,
  author = {W. Goldfard},
  title = {The undecidability of the second order unification problem},
  journal = {Theoretical Computer Science},
  year = {1981},
  volume = {13},
  pages = {225--230},
  note = {http://dx.doi.org/10.1016/0304-3975(81)90040-2Electronic Edition},
  doi = {http://dx.doi.org/10.1016/0304-3975(81)90040-2}
}

@article{Hue:75,
  author = {G. Huet},
  title = {A Unification Algorithm for Typed $-Calculus},
  journal = {Theoretical Computer Science},
  year = {1975},
  volume = {1},
  pages = {27--57},
  note = {http://dx.doi.org/10.1016/0304-3975(75)90011-0Electronic Edition},
  url = {http://dx.doi.org/10.1016/0304-3975(75)90011-0}
}

@article{Hue:73,
  author = {G. Huet},
  title = {The Undecidability of Unification in Third Order Logics},
  journal = {Information and Control},
  year = {1973},
  volume = {22},
  pages = {257--267},
  note = {http://dx.doi.org/10.1016/S0019-9958(73)90301-XElectronic Edition},
  doi = {http://dx.doi.org/10.1016/S0019-9958(73)90301-X}
}

@inproceedings{GH:02,
  author = {Gérard P. Huet},
  title = {Higher Order Unification 30 Years Later},
  booktitle = {TPHOLs},
  year = {2002},
  pages = {3-12},
  url = {http://link.springer.de/link/service/series/0558/bibs/2410/24100003.htm}
}

@techreport{UH:92,
  author = {Ullrich Hustadt},
  title = {Unification and Matching in Church's Original Lambda Calculus},
  year = {92},
  number = {MPI-92-219},
  url = {ftp://ftp.mpi-sb.mpg.de/pub/papers/reports/MPI-I-92-219.dvi.Z}
}

@article{KN:89,
  author = {K. Knight},
  title = {Unification: A Multidisciplinary Survey},
  journal = {ACM Computing Surveys},
  year = {1989},
  volume = {21},
  number = {1},
  pages = {93--124}
}

@article{JL:98,
  author = {Jordi Levy},
  title = {Decidable and Undecidable Second-Order Unification Problems},
  journal = {Lecture Notes in Computer Science},
  year = {1998},
  volume = {1379},
  pages = {47--??},
  url = {http://link.springer-ny.com/link/service/series/0558/bibs/1379/13790047.htm}
}

@techreport{Luc:72,
  author = {C. L. Lucchesi},
  title = {The undecidability of the Unification Problem for Third Order languages},
  school = {University Waterloo},
  year = {1972},
  note = {Report CSRR 2059, }
}

@article{MM:82,
  author = {A. Martelli and U. Montanari},
  title = {An Efficient Unification Algorithm},
  journal = {AMC Transactions on Programming Languages and Systems},
  publisher = {Association of Computing Machinery Press},
  year = {1982},
  volume = {4},
  number = {2},
  pages = {258--282},
  note = {http://doi.acm.org/10.1145/357162.357169Electronic Edition},
  doi = {http://doi.acm.org/10.1145/357162.357169}
}

@article{UMTN:88,
  author = {Ursula Martin and Tobias Nipkow},
  title = {Unification in Boolean rings},
  journal = {Journal of Automated Reasoning},
  year = {1988},
  volume = {4},
  pages = {381--396}
}

@inproceedings{DM:91b,
  author = {D. Miller},
  title = {Unification of Simply Typed Lambda-Terms as Logic Programming},
  booktitle = {Proc. Int. Conference on Logic Programming (Paris)},
  publisher = {MIT Press},
  year = {1991},
  pages = {255--269}
}

@article{Mil:91,
  author = {D. Miller},
  title = {A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification},
  journal = {Journal of Logic and Computation},
  year = {1991},
  volume = {1},
  pages = {253 -- 281},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.8958Electronic Edition }
}

@misc{SMND:97,
  author = {Subrata Mitra and Nachum Dershowitz},
  title = {Matching and Unification in Rewrite Theories},
  year = {1997},
  url = {http://citeseer.ist.psu.edu/52607.html}
}

@techreport{Nar:89,
  author = {P. Narendran},
  title = {Some Remarks On Second Order Unification},
  year = {1989},
  number = {89/356/18},
  note = {http://hdl.handle.net/1880/46585Electronic Edition},
  url = {http://hdl.handle.net/1880/46585}
}

@article{PNFPRS:97,
  author = {Paliath Narendran and Frank Pfenning and Richard Statman},
  title = {On the Unification Problem for Cartesian Closed Categories},
  journal = {Journal of Symbolic Logic.},
  year = {1997},
  volume = {62},
  number = {2},
  pages = {636-647}
}

@inproceedings{Nip:93,
  author = {T. Nipkow},
  title = {Functional Unification of Higher-Order Patterns},
  booktitle = {Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science},
  publisher = {IEEE Computer Society Press},
  year = {1993},
  pages = {64--74},
  note = {http://www4.in.tum.de/~nipkow/pubs/lics93.htmlElectronic Edition},
  url = {http://www4.informatik.tu-muenchen.de/~nipkow/pubs/lics93.html}
}

@inproceedings{FOPNDD:95,
  author = {Friedrich Otto and Paliath Narendran and Daniel J. Dougherty},
  title = {Some Independence Results For Equational Unification},
  booktitle = {Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA-95)},
  publisher = {Springer-Verlag},
  year = {1995},
  volume = {914},
  pages = {367--381}
}

@inproceedings{BPFP:03,
  author = {Brigitte Pientka and Frank Pfenning},
  title = {Optimizing Higher-Order Pattern Unification},
  booktitle = {CADE},
  year = {2003},
  pages = {473-487}
}

@article{CP:94,
  author = {C. Prehofer},
  title = {Decidable higher-order unification problems},
  journal = {Lecture Notes in Computer Science},
  year = {1994},
  volume = {814},
  pages = {635--??}
}

@article{MSSKS:05,
  author = {Manfred Schmidt-Schauß and Klaus U. Schulz},
  title = {Decidability of bounded higher-order unification},
  journal = {Journal of Symbolic Computation},
  year = {2005},
  volume = {40},
  number = {2},
  pages = {905--954}
}

@article{SG:89,
  author = {W. Snyder and J. Gallier},
  title = {Higher Order Unification Revisited: Complete Sets of Transformations},
  journal = {Journal of Symbolic Computation},
  year = {1989},
  volume = {8},
  number = {1 & 2},
  pages = {101--140},
  note = {http://dx.doi.org/10.1016/S0747-7171(89)80023-9Electronic Edition.},
  doi = {http://dx.doi.org/10.1016/S0747-7171(89)80023-9}
}

@article{Sta:81,
  author = {R. Statman},
  title = {On the Existence of Closed Terms in the Typed $ Calculus II: Transformations of Unification Problems},
  journal = {Theoretical Computer Science},
  year = {1981},
  volume = {15},
  number = {3},
  pages = {329--338},
  note = {http://dx.doi.org/10.1016/0304-3975(81)90086-4Electronic Edition},
  doi = {http://dx.doi.org/10.1016/0304-3975(81)90086-4}
}

@article{UPG:04,
  author = {Christian Urban and Andrew M. Pitts and Murdoch Gabbay},
  title = {Nominal unification},
  journal = {Theoretical Computer Science},
  year = {2004},
  volume = {323},
  number = {1-3},
  pages = {473-497},
  doi = {http://dx.doi.org/10.1016/j.tcs.2004.06.016}
}