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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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