# unification stuff

@incollection{dowek-unif-chapter,
title = {Higher-order Unification and Matching},
author = "Gilles Dowek",
booktitle = {{Handbook of Automated Reasoning}},
editor = "A. Robinson and A. Voronkov",
year = "2001",
publisher = "Elsevier and MIT Press",
chapter=16}

@inproceedings{elliot89,
 author = {Conal Elliot},
 title = {Higher-order unification with dependent types},
 booktitle = {Rewriting Techniques and Applications},
 editor = {N. Dershowitz},
 year = {1989},
 pages = {121--136}
 }

@phdthesis{elliot-thesis,
author = "Conal Elliot",
title = {Extensions and Applications of Higher-Order Unification},
year="1990",
month=May,
school={Carnegie Mellon University}}

@incollection{schubert-interp97,
title = {Linear interpolation for the higher-order matching problem},
author = "A. Schubert",
booktitle = {Theory and Practice of Software Development},
editor = "M. Bidoit and M. Dauchet",
year = "1997",
volume=1214,
series="Lecture Notes in Computer Science",
publisher = "Springer-Verlag"}

@article{miller91-patterns,
  Author = "Dale Miller",
  Title = "A Logic Programming Language with Lambda-Abstraction,
    Function Variables, and Simple Unification",
  Journal = "Journal of Logic and Computation",
  Volume = "1",
  Number = "4",
  Pages = "497--536",
  Year = "1991"}

@unpublished{dowek93-second-order-linear,
  author = "G. Dowek",
  title = "A unification algorithm for second-order linear terms",
  note = "Manuscript",
  year = "1993",
  url = "http://www.lix.polytechnique.fr/~dowek/Publi/linear.ps.gz" }

@inproceedings{sss02-bounded,
 author = {Manfred Schmidt-Schau\ss; and Klaus U. Schulz},
 title = {Decidability of Bounded Higher-Order Unification},
 booktitle = {CSL '02: Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic},
 year = {2002},
 isbn = {3-540-44240-5},
 pages = {522--536},
 publisher = {Springer-Verlag},
 address = {London, UK},
}

@inproceedings{ss05-decidable,
  author    = {Manfred Schmidt-Schau\ss},
  editor    = {Dieter Hutter and
               Werner Stephan},
  booktitle = {Mechanizing Mathematical Reasoning, Essays in Honor of J{\"o}rg
               H. Siekmann on the Occasion of His 60th Birthday},
  title = {Decidable Variants of Higher-Order Unification},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2605},
  year      = {2005},
  isbn      = {3-540-25051-4}
}

@article{ss02-stratified,
  Author = "Manfred Schmidt-Schau\ss",
  Title = "A Decision Algorithm for Stratified Context Unification",
  Journal = "Journal of Logic and Computation",
  Volume = "12",
  Number = "6",
  Pages = "929--953",
  Year = "2002"}

@INPROCEEDINGS{levy05-wellnested-cu,
  title = {Well-Nested Context Unification},
  year = {2005},
  author = {Jordi Levy and Joachim Niehren and Mateu Villaret},
  booktitle = {20th International Conference on Automated Deduction},
  month = jun,
  series = {LNAI/LNCS},
  publisher = {Springer Verlag},
  label = {wellnested-cu}
}

@inproceedings{levy96-linear2nd,
 author = {Jordi Levy},
 title = {Linear Second-Order Unification},
 booktitle = {RTA '96: Proceedings of the 7th International Conference on Rewriting Techniques and Applications},
 year = {1996},
 isbn = {3-540-61464-8},
 pages = {332--346},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }

@inproceedings{prehofer94-decidable,
 author = {Christian Prehofer},
 title = {Decidable Higher-Order Unification Problems},
 booktitle = {CADE-12: Proceedings of the 12th International Conference on Automated Deduction},
 year = {1994},
 isbn = {3-540-58156-1},
 pages = {635--649},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }

@article{demoor01higherorder,
    author = "Oege de Moor and Ganesh Sittampalam",
    title = "Higher-order matching for program transformation",
    journal = "Theoretical Computer Science",
    volume = "269",
    number = "1--2",
    pages = "135--162",
    year = "2001"}

@article{goldfarb81-undecidability,
    author = "Warren Goldfarb",
    title = "the undecidability of the second-order unification problem",
    journal = "Theoretical Computer Science",
    volume = "13",
    pages = "225--230",
    year = "1981"}

@article{levy00-undecidability,
author = "Jordi Levy and Margus Veanes",
title = "On the Undecidability of Second-Order Unification",
year = 2000,
journal = "Information and Computation",
volume = 159,
number = "1/2",
pages = "125--150"
}

@incollection{sterling-ho-matching,
author = {Colin Sterling},
title = {A game-theoretic approach to deciding higher-order matching},
booktitle = {ICALP 2006},
editor = "Michele Bugliesi and Bart Preneel and Vladimiro Sassone and Ingo Wegener",
year = "2006",
month = "July",
volume=4052,
series="Lecture Notes in Computer Science",
publisher = "Springer-Verlag"}


