@article{BL:05,
  author = {Bernard Lang,},
  title = {Matching with Multiplication (Extended Abstract)},
  journal = {Mathematical Structures in Computer Science},
  year = {2005},
  volume = {15},
  pages = {959-968},
  note = {http://dx.doi.org/10.1017/S0960129505004883Electronic Edition},
  doi = {http://dx.doi.org/10.1017/S0960129505004883}
}

@article{FBJJMO:08,
  author = {Frédéric Blanqui and Jean-Pierre Jouannaud and Mitsuhiro Okada},
  title = {Inductive-data-type Systems},
  journal = {Theoretical Computer Science},
  publisher = {HAL - CCSD},
  year = {2002},
  volume = {272},
  pages = {41 -- 68},
  url = {http://hal.inria.fr/inria-00105578/en}
}

@inproceedings{HCYJ:97,
  author = {Hubert Comon and Yan Jurski},
  title = {Higher-Order Matching and Tree Automata},
  booktitle = {CSL},
  year = {1997},
  pages = {157-176}
}

@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}
}

@inproceedings{DW:02,
  author = {D. Dougherty and T. Wierzbicki},
  title = {A Decidable Variant of Higher Order Matching},
  booktitle = {RTA '02: Proceedings of the 13th International Conference on Rewriting Techniques and Applications},
  publisher = {Springer Verlag},
  year = {2002},
  volume = {256},
  pages = {340--351},
  note = {http://www.springerlink.com/link.asp?id=y0t2jwqnfucwju35Electronic Edition,}
}

@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}
}

@article{Dow:94,
  author = {G. Dowek},
  title = {Third order matching is decidable},
  journal = {Annals of Pure and Applied Logic},
  year = {1994},
  volume = {69},
  number = {2--3},
  pages = {135--155},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.6700Electronic Edition},
  url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.6700}
}

@article{Dow:93,
  author = {G. Dowek},
  title = {The undecidability of pattern matching in calculi where primitive recursive functions are representable},
  journal = {Theoretical Computer Science},
  publisher = {Elsevier Science Publishers B.V. (North Holland)},
  year = {1993},
  volume = {107},
  pages = {349--356},
  note = {http://dx.doi.org/10.1016/0304-3975(93)90175-SElectronic Edition},
  url = {http://dx.doi.org/10.1016/0304-3975(93)90175-S}
}

@inproceedings{Gro:00,
  author = {P. de Groote},
  title = {Linear Higher-Order Matching Is NP-Complete},
  booktitle = {RTA '00: Proceedings of the 11th International Conference on Rewriting Techniques and Applications},
  publisher = {Springer-Verlag},
  year = {2000},
  volume = {1833},
  pages = {127--140},
  note = {http://portal.acm.org/citation.cfm?id=647199.718705Electronic Edition}
}

@article{PG:00,
  author = {Philippe de Groote},
  title = {Proof-Search in Implicative Linear Logic as a Matching Problem},
  journal = {Lecture Notes in Computer Science},
  year = {2000},
  volume = {1955},
  pages = {257--??},
  url = {http://link.springer-ny.com/link/service/series/0558/bibs/1955/19550257.htm; http://link.springer-ny.com/link/service/series/0558/papers/1955/19550257.pdf}
}

@inproceedings{PGSS:04,
  author = {Philippe de Groote and Sylvain Salvati},
  title = {Higher-Order Matching in the Linear lambda-calculus with Pairing},
  booktitle = {CSL},
  publisher = {Springer},
  year = {2004},
  volume = {3210},
  pages = {220--234},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3210&spage=220}
}

@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{SJJPTZ:02,
  author = {Somesh Jha and Jens Palsberg and Tian Zhao},
  title = {Efficient Type Matching},
  journal = {Lecture Notes in Computer Science},
  year = {2002},
  volume = {2303},
  pages = {187--??},
  url = {http://link.springer-ny.com/link/service/series/0558/bibs/2303/23030187.htm; http://link.springer-ny.com/link/service/series/0558/papers/2303/23030187.pdf}
}

@inproceedings{KT:95,
  author = {T. Kolbe and C. Walther},
  title = {Second-Order Matching modulo Evaluation: A Technique for Reusing Proofs},
  booktitle = {Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence},
  publisher = {Morgan Kaufmann},
  year = {1995},
  pages = {190--195},
  note = {http://www.inferenzsysteme.informatik.tu-darmstadt.de/~walther/Paper/Second-Order-Matching-mod-Eval-IJCAI-1995.pdfElectronic Edition},
  url = {http://www.inferenzsysteme.informatik.tu-darmstadt.de/~walther/Paper/Second-Order-Matching-mod-Eval-IJCAI-1995.pdf}
}

@article{Lo:03,
  author = {R. Loader},
  title = {Higher Order $  Matching is Undecidable},
  journal = {Logic Journal of the IGPL},
  year = {2003},
  volume = {11},
  number = {1},
  pages = {51--68},
  note = {http://dx.doi.org/10.1093/jigpal/11.1.51Electronic Edition},
  doi = {http://dx.doi.org/10.1093/jigpal/11.1.51}
}

@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}
}

@article{OS:01,
  author = {O. de Moor and G. Sittampalam},
  title = {Higher-order matching for program transformation},
  journal = {Theoretical Compuer Science},
  publisher = {Elsevier Science Publishers B.V. (North Holland)},
  year = {2001},
  volume = {269},
  number = {1-2},
  pages = {135--162},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.3784Electronic Edition}
}

@article{Pad:94,
  author = {V. Padovani},
  title = {Decidability of fourth-order matching},
  journal = {Mathematical Structures in Computer Science},
  year = {2000},
  volume = {10},
  pages = {361--372},
  note = {http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=44653Electronic Edition},
  url = {http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=44653}
}

@misc{JPTZ:00,
  author = {Jens Palsberg and Tian Zhao},
  title = {Efficient and Flexible Matching of Recursive Types},
  year = {2000},
  url = {http://citeseer.ist.psu.edu/388882.html; http://www.cs.purdue.edu/homes/tzhao/isomorphism/lics00.ps}
}

@inproceedings{Rit:97,
  author = {M. Rittri},
  title = {Retrieving Library Identifiers via Equational Matching of Types},
  booktitle = {10th International Conference on Automated Deduction},
  publisher = {Springer Verlag},
  year = {1990},
  volume = {449},
  pages = {603-617},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.4344Electronic Edition}
}

@inproceedings{SG:03,
  author = {S. Salvati, P. de Groote},
  title = {On the complexity of higher-order matching in the linear lambda-calculus},
  booktitle = {RTA´03: Rewriting Techniques and Applications, 14th International Conference,},
  publisher = {Springer},
  year = {2003},
  pages = {234--245},
  note = {http://link.springer.de/link/service/series/0558/bibs/2706/27060234.htmElectronic Edition},
  url = {http://link.springer.de/link/service/series/0558/bibs/2706/27060234.htm}
}

@inproceedings{AS:97,
  author = {Aleksy Schubert},
  title = {Linear Interpolation for the Higher-Order Matching Problem},
  booktitle = {TAPSOFT},
  year = {1997},
  pages = {441-452}
}

@unpublished{Col:06,
  author = {C. Stirling},
  title = {Decidability of higher-order matching},
  year = {2008},
  note = {http://homepages.inf.ed.ac.uk/cps/lmcs.psElectronic Edition}
}

@inproceedings{CS:07a,
  author = {Colin Stirling},
  title = {Higher-Order Matching, Games and Automata},
  booktitle = {LICS},
  publisher = {IEEE Computer Society},
  year = {2007},
  pages = {326--335},
  url = {http://doi.ieeecomputersociety.org/10.1109/LICS.2007.23}
}

@inproceedings{CS:07b,
  author = {Colin Stirling},
  title = {Games, Automata and Matching},
  booktitle = {CADE},
  publisher = {Springer},
  year = {2007},
  volume = {4603},
  pages = {1--2},
  url = {http://dx.doi.org/10.1007/978-3-540-73595-3_1}
}

@inproceedings{Col:05,
  author = {C. Stirling},
  title = {Higher-Order Matching and Games},
  booktitle = {Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL Oxford, UK, August 22-25, 2005, Proceedings},
  publisher = {Springer Verlag},
  year = {2005},
  volume = {3634},
  pages = {119--134},
  note = {http://dx.doi.org/10.1007/11538363_10Electronic Edition},
  doi = {http://dx.doi.org/10.1007/11538363_10}
}

@misc{PT:08,
  author = {Paul Tarau},
  title = {Declarative Combinatorics: Boolean Functions, Circuit Synthesis and BDDs in Haskell},
  year = {2008},
  note = {Comment: unpublished draft},
  url = {http://arxiv.org/abs/0808.0760}
}

@incollection{PW:87,
  author = {Philip Wadler},
  title = {Views: A Way for Pattern Matching to Cohabit with Data Abstraction},
  booktitle = {Proceedings, 14th Symposium on Principles of Programming Languages},
  publisher = {Association for Computing Machinery},
  year = {1987},
  pages = {307--312}
}

@inproceedings{TW:99,
  author = {Tomasz Wierzbicki},
  title = {Complexity of the higher order matching},
  booktitle = {CADE},
  year = {1999},
  pages = {82-96},
  url = {http://link.springer.de/link/service/series/0558/bibs/1632/16320082.htm}
}

@inproceedings{RY:05,
  author = {Roy Yoshinaka},
  title = {Higher-Order Matching in the Linear Lambda Calculus in the Absence of Constants Is NP-Complete},
  booktitle = {RTA: Rewriting Techniques and Applications, 1987, LNCS 256},
  year = {2005}
}