@inproceedings{ASvvP:05,
  author = {A. Alimarine, S. Smetsers, A. van Weelden, M. van Eekelen and R. Plasmeijer},
  title = {There and back again: arrows for invertible programming},
  booktitle = {Haskell '05: Proceedings of the 2005 ACM SIGPLAN workshop on Haskell},
  publisher = {ACM Press},
  year = {2005},
  pages = {86--97},
  note = {http://doi.acm.org/10.1145/1088348.1088357Electronic Edition},
  doi = {http://doi.acm.org/10.1145/1088348.1088357}
}

@article{SA:05,
  author = {Samson Abramsky},
  title = {A structural approach to reversible computation},
  journal = {Theoretical Computer Science},
  year = {2005},
  volume = {347},
  number = {3},
  pages = {441--464},
  url = {http://dx.doi.org/10.1016/j.tcs.2005.07.002}
}

@inproceedings{Sam:96,
  author = {Samson Abramsky},
  title = {Semantics and Interaction},
  booktitle = {Semantics and Logics of Computation},
  publisher = {Springer-Verlag},
  year = {1996},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.9567Electronic Edition}
}

@article{SA:93,
  author = {S. Abramsky},
  title = {Computational Interpretations of Linear Logic},
  journal = {Theoretical Computer Science},
  year = {1993},
  volume = {111},
  number = {1-2},
  pages = {3--57}
}

@article{Ack:37,
  author = {W. Ackermann},
  title = {Mengentheoretische Begründung der Logik},
  journal = {Mathematische Annalen},
  year = {1937},
  volume = {114},
  pages = {305--315}
}

@book{AHU:72,
  author = {A. V. Aho and J. E. Hopcroft and J. D. Ullman},
  title = {The design and analysis of computer algorithms},
  publisher = {Addison-Wesley},
  year = {1974}
}

@inproceedings{AASSAvW:05,
  author = {Artem Alimarine and Sjaak Smetsers and Arjen van Weelden and Marko C. J. D. van Eekelen and Rinus Plasmeijer},
  title = {There and back again: arrows for invertible programming},
  booktitle = {Haskell},
  publisher = {ACM},
  year = {2005},
  pages = {86--97},
  url = {http://doi.acm.org/10.1145/1088348.1088357}
}

@misc{EANI:93,
  author = {Eric Allender and U. Polit`ecnica De Catalunya and Neil Immerman},
  title = {A First-Order Isomorphism Theorem},
  year = {1993},
  url = {http://citeseer.ist.psu.edu/47536.html; http://www.cs.umass.edu/~immerman/pub/isomorphism.ps}
}

@article{SAMF:05,
  author = {Sandra Alves and Mário Florido},
  title = {Weak linearization of the lambda calculus},
  journal = {Theoretical Computer Science},
  year = {2005},
  volume = {342},
  number = {1},
  pages = {79--103},
  url = {http://dx.doi.org/10.1016/j.tcs.2005.06.005}
}

@inproceedings{AASS:97,
  author = {Alexander E. Andreev and Sergei Soloviev},
  title = {A Deciding Algorithm for Linear Isomorphism of Types with Complexity O (n log$^2$(n))},
  booktitle = {CTCS},
  publisher = {Springer},
  year = {1997},
  volume = {1290},
  pages = {197--209}
}

@inproceedings{ZAA:91,
  author = {Zena M. Ariola and Arvind},
  title = {A Syntactic Approach to Program Transformations},
  booktitle = {PEPM},
  year = {1991},
  pages = {116--129}
}

@inproceedings{FAJJ:04,
  author = {Frank Atanassow and Johan Jeuring},
  title = {Inferring Type Isomorphisms Generically},
  booktitle = {MPC},
  publisher = {Springer},
  year = {2004},
  volume = {3125},
  pages = {32--53},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3125&spage=32}
}

@other{Automath,
  author = {AUTOMATH},
  title = {The AUTOMATH project},
  year = {1967},
  note = {http://www.win.tue.nl/automath/Website},
  url = {http://www.win.tue.nl/automath/}
}

@article{HB:94,
  author = {Henry G. Baker},
  title = {A "Linear Logic" Quicksort},
  journal = {SIGPLAN Notices},
  year = {1994},
  volume = {29},
  number = {2},
  pages = {13--18}
}

@inproceedings{VBRdC:99,
  author = {Vincent Balat and Roberto Di Cosmo},
  title = {A Linear Logical View of Linear Type Isomorphisms},
  booktitle = {CSL},
  publisher = {Springer},
  year = {1999},
  volume = {1683},
  pages = {250--265}
}

@article{VBOD:02,
  author = {Vincent Balat and Olivier Danvy},
  title = {Memoization in Type-Directed Partial Evaluation},
  journal = {Lecture Notes in Computer Science},
  year = {2002},
  volume = {2487},
  pages = {78--??},
  url = {http://link.springer.de/link/service/series/0558/bibs/2487/24870078.htm; http://link.springer.de/link/service/series/0558/papers/2487/24870078.pdf}
}

@article{FBSB:96,
  author = {Franco Barbanera and Stefano Berardi},
  title = {A Symmetric Lambda Calculus for Classical Program Extraction},
  journal = {Information and Compution},
  year = {1996},
  volume = {125},
  number = {2},
  pages = {103--117}
}

@article{HB:97,
  author = {Henk Barendregt},
  title = {The Impact of the Lambda Calculus on Logic and Computer Science},
  journal = {Bulletin of Symbolic Logic},
  year = {1997},
  volume = {3},
  number = {3},
  pages = {181--215},
  url = {ftp://math.ucla.edu/pub/asl/bsl/0302/0302-003.ps}
}

@incollection{Bar:93,
  author = {H. P. Barendregt},
  title = {Lambda Calculi with Types},
  booktitle = {Handbook of Logic in Computer Science},
  publisher = {Oxford University Press},
  year = {1991},
  volume = {2},
  note = {http://citeseer.ist.psu.edu/barendregt92lambda.htmlElectronic Edition},
  url = {http://citeseer.ist.psu.edu/barendregt92lambda.html and http://www.cs.ru.nl/~henk/Personal Webpage}
}

@book{Bar:84,
  author = {H. P. Barendregt},
  title = {The Lambda Calculus Its Syntax and Semantics},
  publisher = {North Holland},
  year = {1984},
  volume = {103},
  edition = {Revised},
  note = {http://www.cs.ru.nl/~henk/Personal Webpage}
}

@article{Bart:05,
  author = {Barthe, G.},
  title = {A computational view of implicit coercions in Type theory},
  journal = {Mathematical Structures in Computer Science},
  year = {2005},
  volume = {15},
  pages = {839-874},
  note = {http://dx.doi.org/10.1017/S0960129505004901Electronic Edition},
  doi = {http://dx.doi.org/10.1017/S0960129505004901}
}

@inproceedings{Bart:96,
  author = {G. Barthe},
  title = {Implicit Coercions in Type Systems},
  booktitle = {International Workshop TYPES'96},
  publisher = {Springer Verlag},
  year = {1996},
  volume = {1512},
  pages = {1-15},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.9520Electronic Edition}
}

@inproceedings{GBOP:01,
  author = {Gilles Barthe and Olivier Pons},
  title = {Type Isomorphisms and Proof Reuse in Dependent Type Theory},
  booktitle = {FoSSaCS},
  publisher = {Springer},
  year = {2001},
  volume = {2030},
  pages = {57--71},
  url = {http://link.springer.de/link/service/series/0558/bibs/2030/20300057.htm}
}

@article{Bas:94,
  author = {D. Basin},
  title = {A term equality problem equivalent to Graph Isomorphism},
  journal = {Information Processing Letters},
  year = {1994},
  volume = {51},
  number = {2},
  pages = {61--66},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.7354Electronic Edition}
}

@article{Bed:74,
  author = {A. R. Bednarek},
  title = {A note on tree isomorphisms},
  journal = {Journal of Combinatorial Theory Series B},
  publisher = {Academic Press},
  year = {1974},
  volume = {16},
  pages = {194--196},
  note = {http://dx.doi.org/10.1016/0095-8956(74)90064-1Electronic Edition}
}

@article{Ben:73,
  author = {C. H. Bennett},
  title = {Logical Reversibility of Computation},
  journal = {IBM Journal of Research and Development},
  year = {1973},
  volume = {17},
  number = {6},
  pages = {525--532},
  note = {http://www.research.ibm.com/journal/rd/176/ibmrd1706G.pdfElectronic Edition},
  url = {http://www.research.ibm.com/journal/rd/176/ibmrd1706G.pdf}
}

@inproceedings{SB:02,
  author = {Stefan Berghofer},
  title = {Program Extraction in Simply-Typed Higher Order Logic},
  booktitle = {TYPES},
  publisher = {Springer},
  year = {2002},
  volume = {2646},
  pages = {21--38},
  url = {http://link.springer.de/link/service/series/0558/bibs/2646/26460021.htm}
}

@article{JBJK:80,
  author = {Bergstra and Klop},
  title = {Invertible Terms in the Lambda Calculus},
  journal = {Theoretical Computer Science},
  year = {1980},
  volume = {11},
  pages = {19 -- 37}
}

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

@phdthesis{Bet:98,
  author = {G. Betarte},
  title = {Dependent Record Types and Algebraic Structures in Type Theory},
  school = {Department of Computing Science, Chalmers University of Technology and University of Göteborg},
  year = {1998}
}

@article{Bie:97,
  author = {G. M. Bierman},
  title = {A Classical Linear lambda-calculus},
  journal = {Theoretical Computer Science},
  year = {1999},
  volume = {227},
  number = {1-2},
  pages = {43-78},
  note = {http://dx.doi.org/10.1016/S0304-3975(99)00048-1Electronic Edition},
  doi = {http://dx.doi.org/10.1016/S0304-3975(99)00048-1}
}

@inproceedings{BGJ:00,
  author = {R. Bird and J. Gibbons and G. Jones},
  title = {Program Optimisation, Naturally},
  booktitle = {Millenial Perspectives in Computer Science. Palgrave},
  year = {2000},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.2331Electronic Edition},
  doi = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.2331}
}

@book{BO:97,
  author = {R. S. Bird and O. De Moor},
  title = {Algebra of Programming},
  publisher = {Prentice-Hall International Series in Computer Science},
  year = {1997},
  volume = {100},
  note = { http://www.comlab.ox.ac.uk/oucl/publications/books/algebra/Project's Webpage},
  url = {http://www.comlab.ox.ac.uk/oucl/publications/books/algebra/}
}

@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{KBGL:85,
  author = {Bruce and Longo},
  title = {Provable Isomorphisms and Domain Equations in Models of Typed Languages},
  booktitle = {STOC: ACM Symposium on Theory of Computing (STOC)},
  year = {1985}
}

@techreport{KBRdCGL:90,
  author = {Kim B. Bruce and Roberto di Cosmo and Giuseppe Longo},
  title = {Provable Isomorphisms of Types},
  year = {1990},
  number = {90-14}
}

@article{BDL:91,
  author = {K. B. Bruce and R. Di Cosmo and G. Longo},
  title = {Provable isomorphisms of types},
  journal = {Mathematical Structures in Computer Science},
  year = {1991},
  volume = {2},
  number = {2},
  pages = {231--247},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.8353Electronic Edition},
  url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.8353}
}

@article{dB:72,
  author = {N. G. de Bruijn},
  title = {Lambda Calculus Notation with Nameless Dummies, A Tool for Automatic Formula Manipulation, With Applications to the Church-Rosser Theorem},
  journal = {Indagationes Mathematicae (Koninglijke Nederlandse Akademie van Wetenschappen)},
  year = {1972},
  volume = {34},
  number = {5},
  pages = {381--392},
  note = {http://www.win.tue.nl/automath/archive/pdf/aut029.pdfElectronic Edition}
}

@article{BD:77,
  author = {R. M. Burstall and J. Darlington},
  title = {A transformational system for developing recursive programs},
  journal = {Journal of the Associattion of Computing Machinery},
  year = {1977},
  volume = {24},
  number = {1},
  pages = {44--67},
  note = {http://doi.acm.org/10.1145/321992.321996Electronic Edition},
  url = {http://portal.acm.org/citation.cfm?id=321996}
}

@inproceedings{BD:74,
  author = {C. Böhm and M. Dezani-Ciancaglini},
  title = {Combinatorial Problems, Combinator Equations and Normal Forms},
  booktitle = {Proceedings of the 2nd Colloquium on Automata, Languages and Programming},
  journal = {Automata, Languages and Programming, Second Colloquium, Saarbrücken},
  publisher = {Lecture Notes in Computer Science, Springer-Verlag},
  year = {1974},
  volume = {14},
  pages = {185--199},
  note = {http://portal.acm.org/citation.cfm?id=646230.681874Electronic Edition}
}

@techreport{CP:02,
  author = {J. Cai and R. Paige},
  title = {Multiset Discrimination - A Method for Implementing Programming Language Systems without Hashing},
  year = {1992},
  number = {TR1992-609},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.5597Electronic Edition}
}

@article{Car:96,
  author = {L. Cardelli},
  title = {Type systems},
  journal = {ACM Computing Surveys},
  year = {1996},
  volume = {28},
  number = {1},
  pages = {263--264},
  note = {http://doi.acm.org/10.1145/234313.234418Electronic Edition},
  url = {http://www.acm.org/pubs/citations/journals/surveys/1996-28-1/p263-cardelli/}
}

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

@article{SCGG:91,
  author = {Sharad Chaudhary and Gary Gordon},
  title = {Tutte polynomials for trees},
  journal = {Journal Graph Theory},
  publisher = {John Wiley & Sons},
  year = {1991},
  volume = {15},
  number = {3},
  pages = {317--331}
}

@article{Che:05,
  author = {Chemouil, Davis, M.},
  title = {Isomorphisms of simple inductive types through extensional rewriting},
  journal = {Mathematical Structures in Computer Science},
  year = {2005},
  volume = {15},
  pages = {875-915},
  note = {http://dx.doi.org/10.1017/S0960129505004950Electronic Edition},
  doi = {http://dx.doi.org/10.1017/S0960129505004950}
}

@article{CYM:05,
  author = {Yun Chi and Yirong Yang and Richard R. Muntz},
  title = {Canonical forms for labelled trees and their applications in frequent subtree mining},
  journal = {Knowledge and Information Systems.},
  year = {2005},
  volume = {8},
  number = {2},
  pages = {203-234},
  doi = {http://dx.doi.org/10.1007/s10115-004-0180-7}
}

@inproceedings{YCTA:06,
  author = {Y. Chiba and T. Aoto},
  title = {RAPT: A Program Transformation System Based on Term Rewriting (system description)},
  booktitle = {Term Rewriting and Applications, 17th International Conference, RTA-06},
  publisher = {Springer},
  year = {2006},
  pages = {267--276}
}

@inproceedings{OC:99,
  author = {Olaf Chitil},
  title = {Type Inference Builds a Short Cut to Deforestation},
  booktitle = {ICFP},
  year = {1999},
  pages = {249-260},
  url = {http://doi.acm.org/10.1145/317636.317907}
}

@article{Ch:40,
  author = {A. Church},
  title = {A formulation of a simple theory of types},
  journal = {Journal of Symbolic Logic},
  year = {1940},
  volume = {5},
  pages = {56--68},
  note = {http://www.jstor.org/stable/2266866Electronic Edition},
  url = {http://www.jstor.org/stable/2266866}
}

@article{Ch:33,
  author = {A. Church},
  title = {A Set of Postulates for the Foundation of Logic Part II},
  journal = {Annals of Mathematics},
  year = {1933},
  volume = {34},
  number = {2},
  pages = {839--864}
}

@article{Ch:32,
  author = {A. Church},
  title = {A Set of Postulates for the Foundation of Logic Part I},
  journal = {Annals of Mathematics},
  year = {1932},
  volume = {33},
  number = {2},
  pages = {346--366},
  note = {http://www.jstor.org/stable/1968702Electronic Edition},
  url = {http://www.jstor.org/stable/1968702}
}

@article{CR:36,
  author = {A. Church and J. B. Rosser},
  title = {Some properties of conversion},
  journal = {Transactions of the American Mathematical Society},
  year = {1936},
  volume = {39},
  pages = {472--482},
  note = {http://www.jstor.org/stable/2268573Electronic Edition},
  url = {http://www.jstor.org/stable/2268573}
}

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

@techreport{JC:00,
  author = {Jeffrey Considine},
  title = {Efficient Hash-Consing of Recursive Types},
  year = {2000},
  number = {2000-006},
  url = {http://www.cs.bu.edu/techreports/2000-006-hashconsing-recursive-types.ps.Z}
}

@techreport{JC:00b,
  author = {Jeffrey Considine},
  title = {Deciding Isomorphisms of Simple Types in Polynomial Time},
  year = {2000},
  number = {2000-010},
  note = {Wed, 22 Oct 2008 14:29:30 GMT},
  url = {http://www.cs.bu.edu/techreports/2000-010-deciding-simple-type-isomorphisms.ps.Z}
}

@other{METAPRL,
  author = {Robert Constable},
  title = {The Metaprl proof assistant},
  year = {1981},
  note = { http://metaprl.org/Website}
}

@book{DC:95,
  author = {R. Di Cosmo},
  title = {Isomorphisms of Types: from Lambda-calculus to information retrieval and languages design},
  publisher = {Birkhaeuser},
  year = {1995},
  note = {http://books.google.com/books?id=cdJZRjIxavwC&dq=Isomorphisms+of+Types:+from+Lambda-calculus+to+information+retrieval+and+languages+design&source=gbs_summary_s&cad=0Electronic Edition}
}

@article{DiC:95,
  author = {Roberto Di Cosmo},
  title = {Second Order Isomorphic Types: A Proof Theoretic Study on Second Order lambda-Calculus with Surjective Paring and Terminal Object},
  journal = {Information and Compution},
  year = {1995},
  volume = {119},
  number = {2},
  pages = {176-201}
}

@inproceedings{DiCFPDR05,
  author = {Roberto Di Cosmo and Francois Pottier and Didier Rémy},
  title = {Subtyping Recursive Types Modulo Associative Commutative Products},
  booktitle = {TLCA},
  publisher = {Springer},
  year = {2005},
  volume = {3461},
  pages = {179--193},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3461&spage=179}
}

@inproceedings{LCBS:03,
  author = {Luís Cruz-Filipe and Bas Spitters},
  title = {Program Extraction from Large Proof Developments},
  booktitle = {TPHOLs},
  publisher = {Springer},
  year = {2003},
  volume = {2758},
  pages = {205--220},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2758&spage=205}
}

@unpublished{Cur:06,
  author = {Curien, Pierre Louis},
  title = {Notes on Game Semantics},
  year = {2006},
  note = {http://www.pps.jussieu.fr/~curien/Game-semantics.pdfElectronic Edition}
}

@inproceedings{Cu:34,
  author = {H. Curry},
  title = {Functionality in combinatorial logic},
  booktitle = {Proceedings of National Academy of Sciences},
  year = {1934},
  volume = {20},
  pages = {584--590}
}

@book{CF:58,
  author = {H. B. Curry and R. Feys},
  title = {Combinatory Logic, Volume I},
  publisher = {North-Holland},
  year = {1958},
  pages = {xvi+417},
  note = {Second printing 1968}
}

@book{CHS:72,
  author = {H. B. Curry and J. R. Hindley and J. P. Seldin},
  title = {Combinatory Logic, Volume II},
  publisher = {North-Holland},
  year = {1972},
  pages = {xiv+520}
}

@article{DJS:98,
  author = {V. Danos and J.-B. Joinet and H. Schellinx},
  title = {Computational isomorphisms in classical logic},
  journal = {Theoretical Computer Science},
  year = {2003},
  volume = {294},
  number = {3},
  pages = {353 - 378},
  note = {http://dx.doi.org/10.1016/S0304-3975(01)00148-7Electronic Edition},
  doi = {http://dx.doi.org/10.1016/S0304-3975(01)00148-7}
}

@article{VDJJHS97,
  author = {V. Danos and J.-B. Joinet and H. Schellinx},
  title = {A new deconstructive logic: linear logic},
  journal = {Journal of Symbolic Logic},
  year = {1997},
  volume = {62},
  number = {3},
  pages = {755--807},
  note = {footnotesize (Slightly revised version of the 1995 technical report with the same title)}
}

@misc{VDJJHS01,
  author = {Vincent Danos and Jean-baptiste Joinet and Harold Schellinx and Equipe De Logique Mathematique and Universite Paris Vii and Mathematisch Instituut},
  title = {Computational Isomorphisms},
  year = {2001},
  url = {http://citeseer.ist.psu.edu/623841.html; http://www.logique.jussieu.fr/www.danos/psgz/cicl.ps.gz}
}

@book{Dav:82,
  author = {M. Davis},
  title = {Computability and Unsolvability},
  publisher = {Dover},
  year = {1982},
  note = {Previous edition 1958}
}

@article{Dav:73,
  author = {M. Davis},
  title = {Hilbert's Tenth Problem is unsolvable},
  journal = {The American Mathematical Monthly},
  year = {1973},
  volume = {80},
  number = {3},
  pages = {233--269},
  note = {http://www.jstor.org/stable/2318447Electronic Edition},
  url = {http://www.jstor.org/stable/2318447}
}

@inproceedings{Del:00,
  author = {D. Delahaye},
  title = {Information Retrieval in a Coq Proof Library Using Type Isomorphisms},
  booktitle = {TYPES '99: Selected papers from the International Workshop on Types for Proofs and Programs},
  journal = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  year = {2000},
  volume = {1956},
  pages = {131--147},
  note = {http://link.springer.de/link/service/series/0558/bibs/1956/19560131.htmElectronic Edition},
  url = {http://link.springer.de/link/service/series/0558/bibs/1956/19560131.htm}
}

@inproceedings{NDJJJK:95,
  author = {Nachum Dershowitz and Jean-Pierre Jouannaud and Jan Willem Klop},
  title = {Problems in Rewriting III},
  booktitle = {Proceedings of the Sixth International Conference on Rewriting Techniques and Applications (Kaiserslautern, Germany)},
  publisher = {Springer-Verlag},
  year = {1995},
  pages = {457--471}
}

@article{Dez:76,
  author = {M. Dezani-Ciancaglini},
  title = {Characterization of Normal Forms Possesing Inverse in the $beta eta$-Calculus},
  journal = {Theoretical Computer Science},
  year = {1976},
  volume = {2},
  pages = {323--337},
  note = { http://dx.doi.org/10.1016/0304-3975(76)90085-2Electronic Edition},
  url = {http://dx.doi.org/10.1016/0304-3975(76)90085-2}
}

@inproceedings{MDCRdCEGMT:08,
  author = {Mariangiola Dezani-Ciancaglini and Roberto Di Cosmo and Elio Giovannetti and Makoto Tatsuta},
  title = {On Isomorphisms of Intersection Types},
  booktitle = {CSL},
  publisher = {Springer},
  year = {2008},
  volume = {5213},
  pages = {461--477},
  url = {http://dx.doi.org/10.1007/978-3-540-87531-4_33}
}

@article{DT:69,
  author = {J. Doner and A. Tarski},
  title = {An Extended Arithmetic of Ordinal Numbers},
  journal = {Fundamenta Mathematicae},
  year = {1969},
  volume = {65},
  pages = {95--127}
}

@article{KDZP:01,
  author = {Kosta Dosen and Zoran Petric},
  title = {The Typed Bohm Theorem},
  journal = {Electronic Notes in Theoretical Computer Science},
  year = {2001},
  volume = {50},
  number = {2},
  pages = {119 -- 131},
  url = {http://www.elsevier.com/gej-ng/31/29/23/85/28/show/Products/notes/index.htt#003}
}

@article{DDRS00,
  author = {Dougherty and Subrahmanyam},
  title = {Equality between Functionals in the Presence of Coproducts},
  journal = {Information and Computation},
  year = {2000},
  volume = {157},
  pages = {52 -- 83}
}

@inproceedings{Dou:93,
  author = {D. Dougherty},
  title = {Some Lambda Calculi with Categorical Sums and Products},
  booktitle = {Proceedings of Rewriting Techniques and Applications'93},
  year = {1993},
  pages = {137--151},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.6064Electronic 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}
}

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

@inproceedings{DD93,
  author = {Daniel J. Dougherty},
  title = {Some lambda calculi with categorical sums and products},
  booktitle = {Proceedings of the 5th International Conference on Rewriting Techniques and Applications (RTA-93)},
  publisher = {Springer-Verlag},
  year = {1993},
  volume = {690},
  pages = {137--151}
}

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

@article{TELR03,
  author = {Thomas Ehrhard and Laurent Regnier},
  title = {The differential lambda-calculus},
  journal = {Theoretical Computer Science},
  year = {2003},
  volume = {309},
  number = {1--3},
  pages = {1--41}
}

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

@inproceedings{FM:94,
  author = {A. Felty and D. Howe},
  title = {Generalization and Reuse of Tactic Proofs},
  booktitle = {5th International Conference on Logic Programming and Automated Reasoning},
  publisher = {Springer-Verlag },
  year = {1994},
  volume = {822},
  pages = {1--15},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.1064Electronic Edition}
}

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

@inproceedings{FCB:02,
  author = {M. Fiore and R. Di Cosmo and V. Balat},
  title = {Remarks on isomorphisms in typed lambda calculi with empty and sum types},
  booktitle = {Proceedings of Logic in Computer Science'02},
  publisher = {IEEE Computer Society},
  year = {2002},
  pages = {147--156},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.9611Electronic Edition}
}

@misc{Fra:22,
  author = {A. Fraenkel},
  title = {The notion "definite" and the independence of axiom of choice},
  year = {1922}
}

@book{Fre:03,
  author = {G. Frege},
  title = {Grundgesetze der Aritmetik, begriffsschriftlich abgeleitet, Vol. 2},
  publisher = {Jena},
  year = {1904}
}

@book{Fre:93,
  author = {G. Frege},
  title = {Grundgesetze der Aritmetik, begriffsschriftlich abgeleitet, Vol. 1},
  publisher = {Jena},
  year = {1893}
}

@book{Fre:79,
  author = {G. Frege},
  title = {Begriffsschrift, eine der Arithmetischen Nachgebildete Formelsprache des Reinen Denkens},
  publisher = {Halle},
  year = {1879},
  note = {English translation in From Frege to Gödel, a Source Book in Mathematical Logic (J. van Heijenoort, Editor), Harvard University Press, Cambridge, 1967, pp. 1--82}
}

@inproceedings{Fri:75,
  author = {H. Friedman},
  title = {Equality between Functionals.},
  booktitle = {Symposium on Logic Held at Boston, 1972-73},
  publisher = {Springer-Verlag},
  year = {1975},
  volume = {453},
  pages = {22--37}
}

@inproceedings{GP:99,
  author = {Murdoch Gabbay and Andrew M. Pitts},
  title = {A New Approach to Abstract Syntax Involving Binders},
  booktitle = {LICS},
  year = {1999},
  pages = {214-224},
  doi = {http://computer.org/conferen/proceed/lics/0158/01580214abs.htm}
}

@inproceedings{MG:02,
  author = {Murdoch J. Gabbay},
  title = {FM-HOL, a higher-order theory of names},
  booktitle = {35 Years of Automath},
  year = {2002}
}

@phdthesis{MG:00,
  author = {Murdoch J. Gabbay},
  title = {A Theory of Inductive Definitions with $-Equivalence},
  school = {Cambridge University, UK},
  year = {2000}
}

@article{MGAP:02,
  author = {Murdoch J. Gabbay and Andrew M. Pitts},
  title = {A New Approach to Abstract Syntax with Variable Binding},
  journal = {Formal Aspects of Computing},
  year = {2002},
  volume = {13},
  number = {3--5},
  pages = {341--363}
}

@article{JG:00,
  author = {Jeremy Gibbons},
  title = {Generic downwards accumulations},
  journal = {Science of Computer Programming},
  year = {2000},
  volume = {37},
  number = {1-3},
  pages = {37 --65}
}

@incollection{KGGHTA:01,
  author = {Jeremy Gibbons and Graham Hutton and Thorsten Altenkirch},
  title = {When is a Function a Fold or an Unfold?},
  booktitle = {Proc. of 4th Workshop on Coalgebraic Methods in Computer Science, CMCS'01 (Genova, Italy, 6--7 Apr. 2001)},
  publisher = {Elsevier},
  year = {2001},
  volume = {44(1)},
  url = {http://www.cs.nott.ac.uk/~gmh/when.ps}
}

@article{Gil:01,
  author = {J. Gil},
  title = {Subtyping arithmetical types.},
  booktitle = {Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  journal = {SIGPLAN},
  publisher = {ACM Press},
  year = {2001},
  volume = {36},
  number = {3},
  pages = {276-289},
  note = {http://doi.acm.org/10.1145/360204.360232Electronic Edition},
  doi = {http://doi.acm.org/10.1145/373243.360232}
}

@article{JGYZ:07,
  author = {Joseph Gil and Yoav Zibin},
  title = {Randomised algorithms for isomorphisms of simple types},
  journal = {Mathematical Structures in Computer Science},
  year = {2007},
  volume = {17},
  number = {3},
  pages = {565--584},
  url = {http://dx.doi.org/10.1017/S0960129507006068}
}

@article{JGYZ:05,
  author = {Joseph Gil and Yoav Zibin},
  title = {Efficient algorithms for isomorphisms of simple types},
  journal = {Mathematical Structures in Computer Science},
  year = {2005},
  volume = {15},
  number = {5},
  pages = {917--957},
  url = {http://dx.doi.org/10.1017/S0960129505004913}
}

@inproceedings{AGJLSP:93,
  author = {Andrew J. Gill and John Launchbury and Simon L. Peyton Jones},
  title = {A Short Cut to Deforestation},
  booktitle = {FPCA},
  year = {1993},
  pages = {223-232}
}

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

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

@inproceedings{Gu:85,
  author = {R. Gurevič},
  title = {Equational Theory of Positive Numbers with Exponentiation},
  booktitle = {Proceedings of the American Mathematical Society},
  year = {1985},
  volume = {84},
  number = {1},
  pages = {135--141},
  note = {http://www.jstor.org/stable/2044966Electronic Edition},
  url = {http://www.jstor.org/stable/2044966}
}

@article{Gur:90,
  author = {R. Gurevič},
  title = {Equational theory of positive numbers with exponentiation is not finitely axiomatizable},
  journal = {Annals of Pure and Applied Logic},
  year = {1990},
  volume = {49},
  number = {1},
  pages = {1--30},
  note = {http://dx.doi.org/10.1016/0168-0072(90)90049-8Electronic Edition },
  doi = {http://dx.doi.org/10.1016/0168-0072(90)90049-8}
}

@inproceedings{RHCG:93,
  author = {Rachel Harrison and Celia A. Glass},
  title = {Dynamic Programming in a Pure Functional Language},
  booktitle = {Proceedings of the ACM/SIGAPP Symposium on Applied
 Computing},
  year = {1993},
  pages = {179--186},
  url = {http://doi.acm.org/10.1145/162754.162864}
}

@book{vHe:67,
  author = {J. van Heijenoort},
  title = {From Frege to Gödel},
  publisher = {Harvard University Press},
  year = {1967}
}

@phdthesis{Her:30,
  author = {J. Herbrand},
  title = {Recherches sur la théorie de la démonstration},
  school = {Université de Paris},
  year = {1930},
  number = {Thèse de doctorat}
}

@other{Hil:00,
  author = {D. Hilbert},
  title = {The Problems of Mathematics},
  year = {1900},
  note = {http://en.wikipedia.org/wiki/Hilbert's_problemsElectronic Edition},
  url = {http://en.wikipedia.org/wiki/Hilbert's_problems}
}

@book{HS:86,
  author = {J. R. Hindley and J. P. Seldin},
  title = {Introduction or Combinators and Lambda Calculus},
  publisher = {London Mathematical Society Student Texts 1, Cambridge University Press},
  year = {1986}
}

@inproceedings{ZHHIMTAT:97,
  author = {Zhenjiang Hu and Hideya Iwasaki and Masato Takeichi and Akihiko Takano},
  title = {Tupling Calculation Eliminates Multiple Data Traversals},
  booktitle = {ICFP},
  year = {1997},
  pages = {164-175}
}

@article{GH:80,
  author = {Gérard Huet},
  title = {Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems},
  journal = {Journal of the Association for Computing Machinery},
  year = {1980},
  volume = {27},
  number = {4},
  pages = {797--821},
  note = {Preliminary version in it Proceedings, 18th IEEE Symposium on Foundations of Computer Science, IEEE, 1977, pages 30--45}
}

@phdthesis{Hue:76,
  author = {G. Huet},
  title = {Resolution d'Equations dans les langages d'ordre 1, 2,  $},
  school = {Université de Paris VII},
  year = {1976}
}

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

@phdthesis{Hue:72,
  author = {G. Huet},
  title = {Constrained Resolution: A Complete Method for Higher Order Logic},
  school = {Case Western Reserve University},
  year = {1972},
  note = {http://portal.acm.org/citation.cfm?id=906084Electronic Edition}
}

@article{HL:78,
  author = {G. Huet and B. Lang},
  title = {Proving and applying program transformations expressed with second-order patterns},
  journal = {Acta Informatica.},
  publisher = {Springer-Verlag},
  year = {1978},
  volume = {11},
  number = {1},
  pages = {31--55},
  note = {http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/BF00264598Electronic Edition},
  doi = {http://www.springerlink.com/openurl.asp?genre=article\&id=doi:10.1007/BF00264598}
}

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

@article{Hug:89,
  author = {R. J. M. Hughes},
  title = {Why Functional Programming Matters},
  journal = {The Computer Journal},
  year = {1989},
  volume = {32},
  number = {2},
  pages = {98--107},
  note = {http://www.math.chalmers.se/~rjmh/Papers/whyfp.htmlElectronic Edition},
  url = {http://www.math.chalmers.se/~rjmh/Papers/whyfp.html}
}

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

@other{Ocaml,
  author = {INRIA},
  title = {The Objective Caml system},
  year = {Since 1985},
  note = { http://caml.inria.fr/index.en.htmlWebsite}
}

@misc{PJJJ:02,
  author = {Patrik Jansson and Johan Theodoor Jeuring},
  title = {Polytypic Data Conversion Programs},
  year = {2002},
  url = {http://www.library.uu.nl/digiarchief/dip/dispute/2002-0308-100819/2001-34.pdf}
}

@article{JG:95,
  author = {C. B. Jay and N. Ghani},
  title = {The Virtues of Eta-expansion},
  journal = {Journal of Functional Programming},
  year = {1995},
  volume = {5},
  number = {2},
  pages = {135--154},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.613Electronic Edition}
}

@article{BJJKPMJT:06,
  author = {Birgit Jenner and Johannes Köbler and Pierre McKenzie and Jacobo Torán},
  title = {Corrigendum to "Completeness results for graph isomorphism" [J. Comput. System Sci. 66(2003) 549-566]},
  journal = {J. Comput. Syst. Sci},
  year = {2006},
  volume = {72},
  number = {4},
  pages = {783},
  url = {http://dx.doi.org/10.1016/j.jcss.2005.11.002}
}

@misc{BJKL:97,
  author = {Birgit Jenner and Klaus-jorn Lange},
  title = {Tree Isomorphism and Some Other Complete Problems for Deterministic Logspace},
  year = {1997},
  url = {http://citeseer.ist.psu.edu/125009.html; http://www.iro.umontreal.ca/~mckenzie/jelamc97.ps}
}

@inproceedings{BJPMJT:98,
  author = {Birgit Jenner and Pierre McKenzie and Jacobo Torán},
  title = {A Note on the Hardness of Tree Isomorphism},
  booktitle = {Proceedings of the 13th Annual IEEE Conference on Computational Complexity},
  publisher = {IEEE Computer Society Press},
  year = {1998},
  pages = {101--105}
}

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

@article{PJ:05,
  author = {Patricia Johann},
  title = {On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi},
  journal = {Mathematical Structures in Computer Science},
  year = {2005},
  volume = {15},
  number = {2},
  pages = {201--229},
  url = {http://dx.doi.org/10.1017/S0960129504004578}
}

@unpublished{PJJL:98,
  author = {Patricia Johann and John Launchbury},
  title = {Warm Fusion for Masses: Detailing Virtual Data Structure Elimination in Fully Recursive Languages},
  year = {1998},
  note = {Unpublished draft},
  url = {ftp://ftp.cse.ogi.edu/pub/pacsoft/2final_report/wfpaper.ps}
}

@inproceedings{SlP:96,
  author = {Simon L. Peyton Jones},
  title = {Compiling Haskell by Program Transformation: A Report from the Trenches},
  booktitle = {Programming Languages and Systems---ESOP'96},
  publisher = {Springer-Verlag},
  year = {1996},
  volume = {1058},
  pages = {18--44}
}

@article{SPJAS:98,
  author = {Simon L. Peyton Jones and André L. M. Santos},
  title = {A transformation-based optimiser for~Haskell},
  journal = {Science of Computer Programming},
  year = {1998},
  volume = {32},
  number = {1--3},
  pages = {3--47}
}

@misc{SPATTH:01,
  author = {Simon Peyton Jones and Andrew Tolmach and Tony Hoare},
  title = {Playing by the Rules: Rewriting as a practical optimisation technique in GHC},
  year = {2001},
  url = {http://citeseer.ist.psu.edu/464981.html}
}

@inproceedings{AJJT:93,
  author = {Achim Jung and Jerzy Tiuryn},
  title = {A New Characterization of Lambda Definability},
  booktitle = {TLCA},
  year = {1993},
  pages = {245-257}
}

@article{FK:01,
  author = {Fairouz Kamareddine},
  title = {Reviewing the Classical and the de Bruijn Notation for [lambda]-calculus and Pure Type Systems},
  journal = {Journal of Logic and Computation},
  year = {2001},
  volume = {11},
  number = {3},
  pages = {363--394},
  url = {http://www3.oup.co.uk/logcom/hdb/Volume_11/Issue_03/110363.sgm.abs.html}
}

@article{KR:35,
  author = {S. C. Kleene and J. B. Rosser},
  title = {The inconsistency of certain formal logics},
  journal = {The Annals of Mathematics, Second Series},
  year = {1935},
  volume = {36},
  pages = {630--636},
  note = {http://www.jstor.org/stable/1968646Electronic Edition},
  url = {http://www.jstor.org/stable/1968646}
}

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

@incollection{KW:98,
  author = {T. Kolbe and C. Walther},
  title = {Proof Analysis, Generalization, and Reuse},
  booktitle = {Automated Deduction: A Basis for Applications.},
  publisher = {Kluwer Academic Publishers},
  year = {1998},
  volume = {Volume II, Systems and Implementation Techniques},
  note = {http://www.inferenzsysteme.informatik.tu-darmstadt.de/~walther/Paper/Proof_Analysis_Generalization_and_Reuse.psElectronic Edition },
  url = {http://www.inferenzsysteme.informatik.tu-darmstadt.de/~walther/Paper/Proof_Analysis_Generalization_and_Reuse.ps}
}

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

@book{Koz:92,
  author = {D. Kozen},
  title = {The Design and Analysis of Algorithms},
  publisher = {Springer},
  year = {1992},
  note = {http://books.google.com/books?id=L_AMnf9UF9QC&dq=The+Design+and+Analysis+of+Algorithms&source=gbs_summary_s&cad=0Electronic Edition},
  url = {http://books.google.com/books?id=L_AMnf9UF9QC&dq=The+Design+and+Analysis+of+Algorithms&source=gbs_summary_s&cad=0}
}

@inproceedings{KR:03,
  author = {V. Kuncak and M. Rinard},
  title = {Structural Subtyping of Non-Recursive Types is Decidable},
  booktitle = {Proceedings of the Eighteenth Annual IEEE Symp. on Logic in Computer Science},
  publisher = {IEEE Computer Society Press},
  year = {2003},
  pages = {96--107},
  note = {http://citeseer.ist.psu.edu/kuncak03structural.htmlElectronic Edition}
}

@other{ISABELLE,
  author = {L. Paulson, T. Nipkow},
  title = {The ISABELLE theorem prover},
  year = {Since 1989},
  note = {http://www.cl.cam.ac.uk/Research/HVG/Isabelle/Website},
  url = {http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}
}

@techreport{La:94,
  author = {T. Laan},
  title = {A formalization of the Ramified Type Theory},
  year = {1994},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.8847Electronic Edition}
}

@book{LS:86,
  author = {J. Lambek and P. J. Scott},
  title = {Introduction to higher order categorical logic},
  publisher = {Cambridge University Press},
  year = {1986},
  number = {7},
  note = { http://www.andrew.cmu.edu/user/cebrown/notes/lambekscott.htmlElectronic Edition}
}

@article{Lan:61,
  author = {R. Landauer},
  title = {Irreversibility and heat generation in the computing process},
  journal = {IBM-Journal of Research and Development},
  year = {1961},
  volume = {3},
  number = {1/2},
  pages = {183--192},
  note = {http://www.research.ibm.com/journal/rd/441/landauerii.pdfElectronic Edition},
  url = {http://www.research.ibm.com/journal/rd/441/landauerii.pdf}
}

@unpublished{Lat:07,
  author = {Lataillade, Joachim},
  title = {Curry-style type isomorphisms and game semantics},
  year = {2007},
  note = {http://arxiv.org/abs/0705.4228Electronic Edition},
  url = {http://arxiv.org/abs/0705.4228}
}

@article{JdL:07b,
  author = {Joachim De Lataillade},
  title = {Second-Order Type Isomorphisms Through Game Semantics},
  journal = {CoRR},
  year = {2007},
  volume = {abs/0705.4226},
  note = {informal publication},
  url = {http://arxiv.org/abs/0705.4226}
}

@inproceedings{JLTS:95,
  author = {John Launchbury and Tim Sheard},
  title = {Warm Fusion: Deriving Build-Cata's from Recursive Definitions},
  booktitle = {FPCA},
  year = {1995},
  pages = {314-323}
}

@article{Lau:05,
  author = {Laurent, Olivier},
  title = {Classical isomorphisms of types},
  journal = {Mathematical Structures in Computer Science},
  year = {2005},
  volume = {15},
  pages = {969-1004},
  note = {http://dx.doi.org/10.1017/S0960129505004895Electronic Edition},
  doi = {http://dx.doi.org/10.1017/S0960129505004895}
}

@inproceedings{PLJRD:95,
  author = {Pierre Lescanne and Jocelyne Rouyer-Degli},
  title = {Explicit Substitutions with de Bruijn's Levels},
  booktitle = {RTA},
  year = {1995},
  pages = {294-308}
}

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

@inproceedings{PLJM:92,
  author = {P. Lincoln and J. Mitchell},
  title = {Operational Aspects of Linear Lambda Calculus},
  booktitle = {Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science},
  publisher = {IEEE Computer Society Press},
  year = {1992},
  pages = {235--247}
}

@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{Lo:99,
  author = {R. Loader},
  title = {The Undecidability of lambda-Definability},
  year = {1999},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.6860Electronic Edition}
}

@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{Luo:98,
  author = {Z. Luo},
  title = {Coercive Subtyping},
  journal = {Journal of Logic and Computation},
  year = {1999},
  volume = {9},
  number = {1},
  pages = {105--130},
  note = {http://www.dur.ac.uk/CARG/papers/JLC98.ps.gzElectronic Edition},
  url = {http://www.dur.ac.uk/CARG/papers/JLC98.ps.gz},
  doi = {http://dx.doi.org/10.1093/logcom/9.1.105}
}

@inproceedings{MB:02,
  author = {N. Magaud and Y. Bertot},
  title = {Changing Data Structures in Type Theory: A Study of Natural Numbers},
  booktitle = {TYPES, International Workshop on Types for Proofs and Programs},
  journal = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  year = {2000},
  volume = {2277},
  pages = {181 - 196},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.3073Electronic Edition}
}

@unpublished{Mar:04,
  author = {O. J. E. Maroney},
  title = {Are all reversible computations tidy?},
  year = {2004},
  note = {http://arxiv.org/abs/quant-ph/0403079Electronic Edition},
  url = {http://arxiv.org/abs/quant-ph/0403079}
}

@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{Mar:70,
  author = {C. Martin},
  title = {Axiomatic bases for equational theories of natural numbers},
  journal = {Notices of American Mathematical Society},
  year = {1972},
  volume = {19},
  number = {8},
  pages = {778}
}

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

@article{Mat:01,
  author = {Y. Matiyacevich},
  title = {Enumerable sets are Diophantine},
  journal = {Soviet Mathematical},
  year = {1970},
  volume = {11},
  pages = {354--357},
  note = {http://www.jstor.org/stable/2272763Electronic Edition},
  url = {http://www.jstor.org/stable/2272763}
}

@phdthesis{Mc:02,
  author = {B. McAdam},
  title = {Repairing Type Errors in Functional Programs},
  school = {The University of Edinburgh},
  year = {2002},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.3740Electronic Edition}
}

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

@article{DM:91a,
  author = {Dale Miller and Gopalan Nadathur and Frank Pfenning and Andre Scedrov},
  title = {Uniform Proofs as a Foundation for Logic Programming},
  journal = {Annals of Pure and Applied Logic},
  year = {1991},
  volume = {51},
  number = {1--2},
  pages = {125--157}
}

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

@techreport{MYC:03,
  author = {R. R. Muntz and Y. Yang and Y. Chi},
  title = {Mining Frequent Rooted Trees and Free Trees Using Canonical Forms},
  year = {2003},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.8143Electronic Edition}
}

@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{TN:90,
  author = {Tobias Nipkow},
  title = {Proof Transformations for Equational Theories},
  booktitle = {LICS},
  publisher = {IEEE Computer Society},
  year = {1990},
  pages = {278--288}
}

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

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

@inproceedings{Pad:96,
  author = {V. Padovani},
  title = {Decidability of All Minimal Models},
  booktitle = {TYPES '95: Selected papers from the International Workshop on Types for Proofs and Programs},
  journal = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  year = {1996},
  volume = {1158},
  pages = {201--??},
  note = {http://dx.doi.org/10.1007/3-540-61780-9_71Electronic Edition,},
  doi = {http://dx.doi.org/10.1007/3-540-61780-9_71}
}

@inproceedings{Pad:95,
  author = {V. Padovani},
  title = {On equivalence classes of interpolation equations},
  booktitle = {Second International Conference on Typed Lambda Calculi and Applications, TLCA '95 },
  journal = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  year = {1995},
  volume = {902},
  pages = {335--??},
  note = {http://dx.doi.org/10.1007/BFb0014063Electronic Edition},
  doi = {http://dx.doi.org/10.1007/BFb0014063}
}

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

@incollection{AP:98,
  author = {Alberto Pardo},
  title = {Fusion of Monadic (Co)Recursive Programs},
  booktitle = {Informal Proc. of Wksh. on Generic Programming (WGP'98, Marstrand, Sweden, 18 June 1998)},
  publisher = {Dept. of Computing Science, Chalmers Univ. of Techn., and Göteborg Univ.},
  year = {1998},
  note = {Electronic version available at http://wsinwp01.win.tue.nl:1234/WGPProceedings/},
  url = {http://www.fing.edu.uy/~pardo/papers/wgp98.ps.gz}
}

@inproceedings{FPCE:88,
  author = {Frank Pfenning and Conal Elliot},
  title = {Higher-Order Abstract Syntax},
  booktitle = {Proceedings of the ACM SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI)},
  year = {1988},
  pages = {199--208}
}

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

@misc{BP:96,
  author = {Benjamin C. Pierce},
  title = {Foundational Calculi for Programming Languages},
  year = {1996},
  url = {http://citeseer.ist.psu.edu/55202.html; http://www.cs.indiana.edu/ftp/pierce/crchandbook.ps.gz}
}

@article{Pie:06,
  author = {Alessandra Di Pierro and Chris Hankin and Herbert Wiklicky},
  title = {On Reversible Combinatory Logic},
  journal = {Mathematical Structures in Computer Science},
  year = {2006},
  volume = {16},
  number = {4},
  pages = {621--637},
  note = {http://dx.doi.org/10.1016/j.entcs.2005.09.018Electronic Edition},
  doi = {http://dx.doi.org/10.1017/S0960129506005391}
}

@inproceedings{AP:01,
  author = {Andrew M. Pitts},
  title = {Nominal Logic: A First Order Theory of Names and Binding},
  booktitle = {TACS},
  year = {2001},
  pages = {219-242},
  url = {http://link.springer.de/link/service/series/0558/bibs/2215/22150219.htm}
}

@article{AP:00,
  author = {Andrew M. Pitts},
  title = {Parametric polymorphism and operational equivalence},
  journal = {Mathematical Structures in Computer Science},
  year = {2000},
  volume = {10},
  number = {3},
  pages = {321--359}
}

@article{Plo:72,
  author = {G. Plotkin},
  title = {Building in equational theories},
  journal = {Machine Intelligence},
  publisher = {Edinburgh University Press},
  year = {1972},
  volume = {7},
  pages = {73--90},
  note = {http://www.cs.york.ac.uk/mlg/MI/mi.htmlJournal Webpage},
  url = {http://www.cs.york.ac.uk/mlg/MI/mi.html}
}

@inproceedings{RP:93,
  author = {Randy Pollack},
  title = {Closure Under Alpha-Conversion},
  booktitle = {TYPES},
  year = {1993},
  pages = {313-332}
}

@phdthesis{Pre:95,
  author = {C. Prehofer},
  title = {Solving Higher-Order Equations: From Logic to Programming},
  school = {Technische Universität München},
  year = {1995},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.3626Electronic Edition}
}

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

@phdthesis{Pym:90,
  author = {D. Pym},
  title = {Proofs, Search and Computation in General Logic},
  school = {Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh},
  year = {1990},
  number = {CST-69-90},
  note = {http://www.lfcs.inf.ed.ac.uk/reports/90/ECS-LFCS-90-125/Electronic Edition},
  url = {http://www.lfcs.inf.ed.ac.uk/reports/90/ECS-LFCS-90-125/}
}

@other{SML,
  author = {R. Milner, M. Tofte, R. Harper},
  title = {The Standard Meta Language of New Jersey},
  year = {1974},
  note = {http://www.smlnj.org/Website}
}

@inproceedings{FR:99,
  author = {Femke van Raamsdonk},
  title = {Higher-Order Rewriting},
  booktitle = {Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99)},
  publisher = {Springer-Verlag LNCS 1631},
  year = {1999},
  pages = {45--59},
  note = {Invited Tutorial}
}

@article{SRPZ:00,
  author = {Sarnath Ramnath and Peiyi Zhao},
  title = {On the isomorphism of expressions},
  journal = {Information and Processing Letters.},
  publisher = {Elsevier Science B.V. (North Holland)},
  year = {2000},
  volume = {74},
  number = {3-4},
  pages = {97--102}
}

@article{Ram:25,
  author = {F. P. Ramsey},
  title = {The Foundations of Mathematics},
  journal = {Proceedings of the London Mathematical Society, Series 2},
  year = {1925},
  volume = {25},
  number = {5},
  pages = {338--384}
}

@article{JR:95,
  author = {Jon G. Riecke},
  title = {Statman's 1-Section Theorem},
  journal = {Information and Computation},
  year = {1995},
  volume = {116},
  pages = {275--293}
}

@article{Rit:91,
  author = {M. Rittri},
  title = {Using types as search keys in function libraries},
  journal = {Journal of Functional Programming},
  year = {1991},
  volume = {1},
  number = {1},
  pages = {71--89},
  note = {http://dx.doi.org/10.1145/99370.99384Electronic Edition},
  url = {http://dx.doi.org/10.1145/99370.99384}
}

@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{Rob:69,
  author = {J. A. Robinson},
  title = {Mechanizing Higher-Order Logic},
  booktitle = {Machine Intelligence },
  publisher = {Edinburgh University Press},
  year = {1969},
  volume = {4},
  pages = {151--170},
  note = {Journal http://www.cs.york.ac.uk/mlg/MI/mi.htmlJournal Webpage},
  url = {http://www.cs.york.ac.uk/mlg/MI/mi.html}
}

@inproceedings{Rob:67,
  author = {J. A. Robinson},
  title = {A Review of Automatic Theorem-Proving},
  booktitle = {Proceedings of Annual Symposium in Applied Mathematics XIX},
  year = {1967},
  pages = {1--18}
}

@article{Rob:65,
  author = {J. A. Robinson},
  title = {A machine-oriented logic based on the resolution principle},
  journal = {Journal of the ACM},
  year = {1965},
  volume = {12},
  number = {1},
  pages = {23--41},
  note = {http://doi.acm.org/10.1145/321250.321253Electronic Edition},
  doi = {http://doi.acm.org/10.1145/321250.321253}
}

@inproceedings{RW:91,
  author = {E. Rollins and J. Wing},
  title = {Specifications as Search Keys for Software Libraries},
  booktitle = {8th International Conference on Logic Programming},
  publisher = {MIT press},
  year = {1991},
  pages = {173--187},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.8746Electronic Edition}
}

@article{RT:91,
  author = {C. Runciman and I. Toyn},
  title = {Retrieving Reusable Software Components by Polymorphic Type},
  journal = {Journal of Functional Programming},
  year = {1991},
  volume = {1},
  number = {2},
  pages = {191--211},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.6545Electronic Edition}
}

@article{Rus:08,
  author = {B. Russell},
  title = {Mathematical logic as based on the theory of types},
  journal = {American Journal of Mathematics},
  year = {1908},
  volume = {30},
  pages = {222--262},
  note = {http://www.jstor.org/stable/2369948Electronic Edition},
  url = {http://www.jstor.org/stable/2369948}
}

@book{Rus:03,
  author = {B. Russell},
  title = {The Principles of Mathematics},
  publisher = {Cambridge University Press},
  year = {1903}
}

@other{HASKELL,
  author = {S. P. Lones, P. Walder},
  title = {Haskell: A purely functional programming language},
  year = {1990},
  note = { http://www.haskell.org/Website}
}

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

@article{YS:03,
  author = {Yiannakis Sazeides},
  title = {Instruction-Isomorphism in Program Execution},
  journal = {Journal of Instruction-Level Parallelism},
  year = {2003},
  volume = {5},
  url = {http://www.jilp.org/vol5/v5paper13.pdf}
}

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

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

@article{Sel:01,
  author = {Peter Selinger},
  title = {Control Categories and Duality: On the Categorical Semantics of the Lambda-Mu Calculus},
  journal = {Mathematical Structures in Computer Science},
  year = {2001},
  volume = {11},
  number = {2},
  pages = {207-260},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.389Electronic Edition}
}

@article{RS:75,
  author = {Ravi Sethi},
  title = {Errata: ``Testing for the Church-Rosser Property''},
  journal = {Journal of the ACM},
  year = {1975},
  volume = {22},
  number = {3},
  pages = {424--424},
  note = {See teSethi:1974:TCR.}
}

@incollection{PSFdV:02,
  author = {Paula Severi and Fer-Jan de Vries},
  title = {An Extensional Böhm Model},
  booktitle = {Proc. of 13th Int. Conf. on Rewriting Theory and Applications, RTA 2002, Copenhagen, Denmark, 22--24 July 2002},
  publisher = {Springer-Verlag},
  year = {2002},
  volume = {2378},
  pages = {159--173}
}

@article{RSDT:99,
  author = {Ron Shamir and Dekel Tsur},
  title = {Faster subtree isomorphism},
  journal = {Journal of Algorithms},
  publisher = {Academic Press},
  year = {1999},
  volume = {33},
  number = {2},
  pages = {267--280}
}

@article{JS:95,
  author = {Joseph R. Shoenfield},
  title = {The Mathematical Work of S. C. Kleene},
  journal = {Bulletin of Symbolic Logic},
  year = {1995},
  volume = {1},
  pages = {9--43}
}

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

@inproceedings{Sol:93,
  author = {S. Soloviev},
  title = {A Complete Axiom System for Isomorphism of Types in Closed Categories},
  booktitle = {LPAR '93: Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning},
  publisher = {Springer-Verlag},
  year = {1993},
  volume = {698},
  pages = {360--371},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.1383Electronic Edition}
}

@article{Sol:83,
  author = {S. Soloviev},
  title = {The category of finite sets and cartesian closed categories},
  journal = {Journal of Soviet Mathematics (Doklady Mathematics)},
  year = {1983},
  volume = {22},
  pages = {1387--1400},
  note = {http://www.maik.rssi.ru/cgi-bin/journal.pl?name=danmathJournal Webpage},
  url = {http://www.maik.rssi.ru/cgi-bin/journal.pl?name=danmath&page=main}
}

@article{RS:04,
  author = {Richard Statman},
  title = {On the lambda Y calculus},
  journal = {Annals of.Pure and Applied Logic},
  year = {2004},
  volume = {130},
  number = {1-3},
  pages = {325--337},
  url = {http://dx.doi.org/10.1016/j.apal.2004.04.00}
}

@article{RS:82,
  author = {R. Statman},
  title = {Completeness, Invariance and $-definability},
  journal = {Journal of Symbolic Logic},
  year = {1982},
  volume = {47},
  pages = {17--26}
}

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

@incollection{Sta:80,
  author = {R. Statman},
  title = {On the Existence of Closed Terms in the Typed $-Calculus I},
  booktitle = {To H.~B.~Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism},
  publisher = {Academic Press},
  year = {1980},
  pages = {511--534}
}

@inproceedings{GS:94,
  author = {Guy L. Steele},
  title = {Building Interpreters by Composing Monads},
  booktitle = {Principles of Programming Languages},
  year = {1994},
  url = {http://www-swiss.ai.mit.edu/ftpdir/users/dae/related-papers/steele.ps.Z}
}

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

@article{Col:07,
  author = {Stirling, C.},
  title = {Model-Checking Games for Typed Lambda-Calculi},
  journal = {Electronic Notes in Theoretical Computer Science},
  year = {2007},
  volume = {172},
  number = {172},
  pages = {589-609},
  note = {http://dx.doi.org/10.1016/j.entcs.2007.02.021Electronic Edition},
  doi = {http://dx.doi.org/10.1016/j.entcs.2007.02.021}
}

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

@book{PT:99,
  author = {P. Taylor},
  title = {Practical Foundations of Mathematics},
  publisher = {Cambridge University Press},
  year = {1999},
  note = {http://www.cs.man.ac.uk/~pt/Practical_Foundations/html/summary.htmlElectronic Edition}
}

@article{SaT:91,
  author = {Satish R. Thatte},
  title = {Coercive Type Isomorphism},
  journal = {Lecture Notes in Computer Science},
  year = {1991},
  volume = {523},
  pages = {29--??}
}

@inproceedings{ST:04,
  author = {Simon Thompson},
  title = {Refactoring Functional Programs},
  booktitle = {Advanced Functional Programming},
  year = {2004},
  pages = {331-357},
  doi = {http://dx.doi.org/10.1007/11546382_9}
}

@inproceedings{ST:89,
  author = {S. Thompson},
  title = {Functional Programming: Executable Specifications and Program Transformation},
  booktitle = {Proceedings of the 5th International Workshop on Software Specification and Design},
  publisher = {IEEE Computer Society Press},
  year = {1989},
  pages = {287--290}
}

@article{Tur:37,
  author = {A. Turing},
  title = {Computability and $-definability},
  journal = {Journal Symbolic Logic},
  year = {1937},
  volume = {2},
  number = {4},
  pages = {153--163},
  note = {http://www.jstor.org/stable/2268280Electronic Edition},
  url = {http://www.jstor.org/stable/2268280}
}

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

@misc{EV:02,
  author = {Eelco Visser},
  title = {A Survey of Rewriting Strategies in Program Transformation Systems},
  year = {2002},
  url = {http://www.library.uu.nl/digiarchief/dip/dispute/2002-0308-093116/2001-31.pdf}
}

@incollection{PW:94,
  author = {Philip Wadler},
  title = {Monads for functional programming},
  booktitle = {Program Design Calculi},
  publisher = {Springer Verlag},
  year = {1994},
  volume = {118},
  note = {Proceedings of the International Summer School at Marktoberdorf directed by F. L. Bauer, M. Broy, E. W. Dijkstra, D. Gries, and C. A. R. Hoare}
}

@incollection{PW:93,
  author = {Philip Wadler},
  title = {A taste of linear logic},
  booktitle = {Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, MFCS'93 (Gdańsk, Poland, August 30 - September 3, 1993)},
  publisher = {Springer-Verlag},
  year = {1993},
  volume = {711},
  pages = {185--210},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=711&spage=185}
}

@inproceedings{Wad:89,
  author = {P. Wadler},
  title = {Theorems for Free},
  booktitle = {4th International Conference on Functional Programming Languages and Computer Architecture'89.},
  publisher = {ACM Press},
  year = {1989},
  pages = {347--359},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875Electronic Edition}
}

@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{Wan:86,
  author = {M. Wand},
  title = {Finding the Source of Type Errors},
  booktitle = {Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages},
  publisher = {ACM Press},
  year = {1986},
  pages = {38--43},
  note = {http://doi.acm.org/10.1145/512644.512648Electronic Edition},
  doi = {http://doi.acm.org/10.1145/512644.512648}
}

@book{WR:25,
  author = {A. N. Whitehead and B. Russell},
  title = {Principia Mathematica},
  publisher = {Cambridge University Press},
  year = {1925--1927},
  edition = {Second},
  note = {Three volumes.}
}

@book{WR:10,
  author = {A. N. Whitehead and B. Russell},
  title = {Principia Mathematica},
  publisher = {Cambridge University Press},
  year = {1910--1913},
  edition = {First},
  note = {Three volumes.}
}

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

@article{Wil:81,
  author = {A. J. Wilkie},
  title = {On Exponentiation - A Solution to Tarski's High School Algebra Problem},
  journal = {Quaderni di Matematica},
  year = {2000},
  volume = {6},
  pages = {107--129},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.9695Electronic Edition}
}

@inproceedings{XP:99,
  author = {H. Xi and F. Pfenning},
  title = {Dependent Types in Practical Programming},
  booktitle = {In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages},
  publisher = {ACM Press},
  year = {1999},
  pages = {214--227},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.548Electronic Edition}
}

@article{TYJACLAM:00,
  author = {Toshiyuki Yamada and Jürgen Avenhaus and Carlos Loria-Sáenz and Aart Middeldorp},
  title = {Logicality of conditional rewrite systems},
  journal = {Theoretical Computer Science},
  year = {2000},
  volume = {236},
  number = {1--2},
  pages = {209--232},
  url = {http://www.elsevier.nl/gej-ng/10/41/16/168/21/27/abstract.html}
}

@article{YHT:04,
  author = {Yokoyama and Hu and Takeichi},
  title = {Deterministic Second-Order Patterns},
  journal = {Information Processing Letters},
  year = {2004},
  volume = {89},
  number = {6},
  pages = {309 -314},
  note = {http://dx.doi.org/10.1016/j.ipl.2003.12.008Electronic Edition},
  doi = {http://dx.doi.org/10.1016/j.ipl.2003.12.008}
}

@inproceedings{TYZHMT:03,
  author = {Tetsuo Yokoyama and Zhenjiang Hu and Masato Takeichi},
  title = {Deterministic Higher-Order Patterns for Program Transformation},
  booktitle = {LOPSTR},
  year = {2003},
  pages = {128-142},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3018&spage=128}
}

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

@misc{Zer:08,
  author = {E. Zermelo},
  title = {A new proof of the possibility of a well ordering},
  year = {1908}
}

@inproceedings{ZGC:03,
  author = {Zibin and Gil and Considine},
  title = {Efficient Algorithms for Isomorphisms of Simple Types},
  booktitle = {30th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages},
  publisher = {ACM Press},
  year = {2003},
  pages = {160 - 171},
  note = {http://dx.doi.org/10.1017/S0960129505004913Electronic Edition},
  doi = {http://dx.doi.org/10.1017/S0960129505004913}
}

@article{Zul:01,
  author = {P. Zuliani},
  title = {Logical reversibility},
  journal = {IBM-Journal of Research and Development},
  year = {2001},
  volume = {45},
  number = {6},
  pages = {807--818},
  note = {http://www.research.ibm.com/journal/rd/456/zuliani.htmlElectronic Edition},
  url = {http://www.research.ibm.com/journal/rd/456/zuliani.html}
}

@other{Coq,,
  title = {The Coq Proof Assistant},
  year = {1992},
  note = { http://coq.inria.fr/Website},
  url = {http://coq.inria.fr/}
}

@other{PVS,,
  title = {PVS Specification and Verification System},
  year = {1992},
  note = { http://pvs.csl.sri.com/Website},
  url = {http://pvs.csl.sri.com/}
}