%journals
@string{ic = "Information and Computation"}
@string{jacm = "Journal of the Association for Computing Machinery"}
@string{jsl = "Journal of Symbolic Logic"}
@string{jcss = "Journal of Computer and System Sciences"}
@string{am = "Annals of Mathematics"}
@string{jlc = "Journal of Logic and Computation"}
@string{apal = "Annals of Pure and Applied Logic"}
@string{tams = "Transactions of the Americal Mathematical Society"}
@string{mscs = "Mathematical Structures in Computer Science"}
@string{aml = "Archive for Mathematical Logic"}
@string{ma = "Mathematische Annalen"}
@string{jfp = "Journal of Functional Programming"}

%publishers
@string{nh = "North-Holland Publishing Company"}
@string{cup = "Cambridge University Press"}
@string{oup = "Oxford University Press"}
@string{esp= "Elsevier Science Publishers B.V."}
@string{es = "Elsevier Science B.V."}
@string{sv = "Springer Verlag"}
@string{mitp = "MIT Press"}
@string{ieee = "IEEE Computer Society Press"}
@string{pup = "Princeton University Press"}
@string{ap = "Academic Press"}
@string{m = "Masson"}

%series
@string{slfm = "Studies in Logic and the Foundations of Mathematics"}
@string{mct = "Mathematical Centre Tracts"}
@string{cttcs = "Cambridge Tracts in Theoretical Computer Science"}
@string{lncs = "Lecture Notes in Computer Science"}
@string{lmsst = "London Mathematical Society Student Texts"}

\hyphenation{or-tho-go-na-li-ty}

@UNPUBLISHED{Acz:78,
  AUTHOR = "Aczel, Peter",
  TITLE  = "A General {C}hurch-{R}osser Theorem",
  MONTH  = jul,
  YEAR   = "1978",
  NOTE   = "University of Manchester",
}

@INPROCEEDINGS{Aka:93,
  AUTHOR    = "Akama, Yohji",
  TITLE     = "On {M}ints' Reduction  for ccc-Calculus",
  BOOKTITLE = "Proceedings of the International Conference on
              Typed Lambda Calculi and Applications 
              (TLCA '93)",
  YEAR      = 1993,
  EDITOR    = "Bezem, M. and Groote, J.F.",
  PAGES     = "1--12",
  ADDRESS   = "Utrecht, The Netherlands",
  MONTH     = mar,
  NOTE      = "Volume 664 of Lecture Notes in Computer Science"
}


@INPROCEEDINGS{Ant:Mid:94,
  AUTHOR    = "Antoy, Sergio and Middeldorp, Aart",
  TITLE     = "A sequential Reduction Strategy",
  BOOKTITLE = "Proceedings of the 4th International
               Conference on Algebraic and Logic Programming
              (ALP '94)",
  YEAR      = 1994,
  PAGES     ="168--185",
  SERIES    = lncs,
  NUMBER    = 850,
  ADDRESS   = "Madrid"
}

@ARTICLE{Asp:91,
  AUTHOR   = "Asperti, Andrea",
  TITLE    = "Linear Logic, Comonads and Optimal Reductions",
  JOURNAL  = "Fundamenta Informaticae",
  YEAR     = 1994,
  VOLUME   = 22,
  PAGES    = "3--22",
  NOTE     = "Special Issue devoted to Categories in 
             Computer Science"
}

@INPROCEEDINGS{Asp:95,
  AUTHOR    = "Asperti, Andrea",
  TITLE     = "$\delta \ \circ \ ! \epsilon = 1$",
  BOOKTITLE = "Proceedings of the 6th International Conference
              on Rewriting Techniques and Applications
              (RTA '95)",
  YEAR      = 1995,
  EDITOR    = "Hsiang, Jieh",
  PAGES     = "102--116",
  ADDRESS   = "Kaiserslautern, Germany",
  MONTH     = apr,
  SERIES    = lncs,
  NUMBER    = 914
}

@ARTICLE{Asp:Lan:94,
  AUTHOR  = "Asperti, Andrea and Laneve, Cosimo",
  TITLE   = "Interaction Systems {I}:
            The theory of optimal reductions",
  JOURNAL = mscs,
  YEAR    = 1994,
  VOLUME  = 4,
  PAGES   = "457--504"
}

@ARTICLE{Asp:Lan:96,
  AUTHOR  = "Asperti, Andrea and Laneve, Cosimo", 
  TITLE   ="Interaction Systems {II}:
            The practice of optimal reductions",
  JOURNAL = tcs,
  YEAR    = 1996,
  MONTH   = jul,
  NOTE    = "To appear."
}

@PHDTHESIS{Bar:71,
  AUTHOR  = "Barendregt, H.P.",
  TITLE   = "Some Extensional Term Models for Combinatory Logics
            and $\lambda$-calculi",
  SCHOOL  = "Rijksuniversiteit Utrecht",
  YEAR    = 1971
}

@ARTICLE{Bar:74,
  AUTHOR  = "Barendregt, H.P.",
  TITLE   = "Pairing without conventional constraints",
  JOURNAL = "Zeitschrift f{\"u}r mathematischen Logik
            und Grundlagen der Mathematik",
  YEAR    = 1974,
  VOLUME  = 20,
  PAGES   = "289--306"
}


@BOOK{Bar:84,
  AUTHOR    = "Barendregt, H.P.",
  TITLE     = "The Lambda Calculus, its Syntax and Semantics",
  PUBLISHER = nh,
  YEAR      = 1984,
  VOLUME    = 103,
  SERIES    = slfm,
  EDITION   = "Revised",
}

@INCOLLECTION{Bar:92,
  AUTHOR    = "Barendregt, H.P.",
  TITLE     = "Lambda calculi with types",
  BOOKTITLE = "Handbook of Logic in Computer Science",
  PUBLISHER = oup,
  YEAR      = 1992,
  EDITOR    = "Abramsky, S. and Gabbay, Dov M. and Maibaum, T.S.E",
  PAGES     = "117--310",
  ADDRESS   = "New  York",
  VOLUME    = 2
}

@TECHREPORT{Bar:Ber:Klo:Vol:76,
  AUTHOR      = "Barendregt, Henk and
                Bergstra, Jan and
                Klop, Jan Willem and
                Volken, Henri",
  TITLE       = "Degrees, Reductions and Representability in the
                Lambda Calculus",
  INSTITUTION = "University Utrecht",
  NUMBER      = 22,
  YEAR        = 1976,
  MONTH       = feb
}

@ARTICLE{Ber:Klo:86,
  AUTHOR  = "Bergstra, J.A. and Klop, J.W.",
  TITLE   = "Conditional Rewrite Rules: Confluence and Termination",
  JOURNAL = jcss,
  YEAR    = 1986,
  VOLUME  = 32,
  PAGES   = "323--362",
}

@INCOLLECTION{Bou:85,
  AUTHOR    = "Boudol, G.",
  TITLE     = "Computational semantics of term rewriting systems",
  BOOKTITLE = "Algebraic methods in semantics",
  PUBLISHER = cup,
  YEAR      = 1985,
  EDITOR    = "Nivat, Maurice and Reynolds, John C.",
  CHAPTER   = "5",
  PAGES     = "169--236",
}



@ARTICLE{Bre:Gal:90,
  AUTHOR  = "Breazu-Tannen, Val and Gallier, Jean",
  TITLE   = "Polymorphic rewriting conserves 
            algebraic strong normalization",
  JOURNAL = tcs,
  YEAR    = 1990,
  VOLUME  = 83,
  PAGES   = "3--28"
}

@ARTICLE{Bre:Gal:94,
  AUTHOR  = "Breazu-Tannen, Val and Gallier, Jean",
  TITLE   = "Polymorphic rewriting conserves 
            algebraic confluence",
  JOURNAL = ic,
  VOLUME  = 14,
  NUMBER  = 1,
  PAGES   = "1--29",
  YEAR    = 1994
}

@BOOK{Chu:41,
  AUTHOR     = "Church, A.",
  TITLE      = "The Calculi of Lambda Conversion",
  PUBLISHER  = pup,
  YEAR       = 1941
}

@ARTICLE{Chu:Ros:36,
  AUTHOR  = "Church, Alonzo and Rosser, J.B.",
  TITLE   = "Some properties of conversion",
  JOURNAL = tams,
  YEAR    = 1936,
  VOLUME  = 39,
  PAGES   = "472--482"
}

@ARTICLE{Coq:Hue:88,
  AUTHOR  = "Coquand, Th. and Huet, G.",
  TITLE   = "The calculus of constructions",
  JOURNAL = ic,
  YEAR    = 1988,
  VOLUME  = 76,
  PAGES   = "95--120"
}



@UNPUBLISHED{Cub:93,
  AUTHOR = "{\v C}ubri{\v c}, Djordje",
  TITLE  = "Embedding of a free cartesian closed category
           into the category of sets",
  YEAR   = 1993,
  NOTE   = "McGill University"
}

@BOOK{Cur:93,
  AUTHOR    = "Curien, Pierre-Louis",
  TITLE     = "Categorical Combinators, Sequential Algorithms,  
              and Functional Programming",
  PUBLISHER = "Birkh{\"a}user",
  YEAR      = 1993,
  ADDRESS   = "Boston, USA",
  NOTE      = "Second edition"
}

@TECHREPORT{Cur:95,
  AUTHOR      = "Curien, Pierre-Louis",
  TITLE       = "Alg{\`e}bre Universelle,
                Introduction au $\lambda$-calcul et aux Logiques
                Combinatoires (Notes de Cours)",
  INSTITUTION = "Ecole Normale Sup{\'e}riere",
   NUMBER      = "LIENS-95-30",
  MONTH       = nov,
  YEAR        = 1995
}



@BOOK{Cur:Fey:Cra:58,
  AUTHOR    = "Curry, Haskell B. and Feys, Robert and Craig, William",
  TITLE     = "Combinatory Logic, volume I",
  PUBLISHER = nh,
  YEAR      = 1958,
  SERIES    = slfm,
  ADDRESS   = "Amsterdam",
}

@PHDTHESIS{Dan:90,
  AUTHOR  = "Danos, Vincent",
  TITLE   = "La Logique Lin{\'e}aire appliqu{\'e}e {\`a}
            l'{\'e}tude de divers processus de normalisation
            (principalement du $\lambda$-calcul)",
  SCHOOL  = "Universit{\'e} Paris {VII}",
  YEAR    = 1990
}

@ARTICLE{Dan:Reg:89,
  AUTHOR  = "Danos, Vincent and R{\'e}gnier, Laurent",
  TITLE   = "The structure of multiplicatives",
  JOURNAL = aml,
  YEAR    = 1989,
  VOLUME  = 28,
  PAGES   = "181--203"
}



@INCOLLECTION{Der:Jou:90,
  AUTHOR    = "Dershowitz, Nachum and Jouannaud, Jean-Pierre",
  TITLE     = "Rewrite Systems",
  BOOKTITLE = "Handbook of Theoretical Computer Science",
  PUBLISHER = esp,
  YEAR      = 1990,
  EDITOR    = "Leeuwen, Jan van",
  CHAPTER   = 6,
  VOLUME    = "B: Formal Models and Semantics",
  PAGES     = "243--320",
  ADDRESS   = "Amsterdam",
}

@ARTICLE{DiC:Kes:94,
  AUTHOR  = "Di Cosmo, Roberto and Kesner, Delia",
  TITLE   = "Simulating Expansions Without Expansions",
  JOURNAL = mscs,
  YEAR    = 1994,
  VOLUME  = 4,
  PAGES   = "315--362"
}

@TECHREPORT{Fer:Sev:93,
  AUTHOR      = "Ferrer, Walter and Severi, Paula",
  TITLE       = "Abstract Reduction and Topology",
  INSTITUTION = "Eindhoven University of Technology",
  NUMBER      = "93/35",
  MONTH       = oct,
  YEAR        = 1993
}


@PHDTHESIS{Fie:91,
  AUTHOR  = "Field, John Henry",
  TITLE   = "Incremental Reduction in the Lambda Calculus and
            Related Reduction Systems",
  SCHOOL  = "Cornell University",
  YEAR    = 1991,
  ADDRESS = "Ithaca, New York, USA"
}

@INPROCEEDINGS{Fie:93,
  AUTHOR    = "Field, John",
  TITLE     = "A graph reduction approach to 
              incremental term rewriting",
  BOOKTITLE = "Proceedings of the Fifth International Conference
              on Rewriting Techniques and Application (RTA '93)",
  YEAR      = 1993,
  EDITOR    = "Kirchner, Claude",
  PAGES     = "259--273",
  ADDRESS   = "Montreal, Canada",
  MONTH     = jun,
  SERIES    = lncs,
  NUMBER    = 690
}

@INCOLLECTION{Gan:80,
  AUTHOR    = "Gandy, R.O.",
  TITLE     = "Proofs of Strong Normalization",
  BOOKTITLE = "To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus
              and Formalism",
  PUBLISHER = ap,
  YEAR      = 1980,
  EDITOR    = "Seldin, J.P. and Hindley, J.R.",
  PAGES     = "457--477"
}


@INPROCEEDINGS{Gar:94,
  AUTHOR    = "Gardner, Phillipa",
  TITLE     = "Discovering Needed Reductions 
              Using Type Theory",
  BOOKTITLE = "Proceedings of the Second International Symposium
              on Theoretical Aspects of Computer Software (TACS '94)",
  YEAR      = 1994,
  EDITOR    = "Hagiya, Masami and Mitchell, John C.",
  PAGES     = "555--574",
  ADDRESS   = "Sendai, Japan",
  MONTH     = apr,
  SERIES    = lncs,
  NUMBER    = 789
}

@INPROCEEDINGS{Ghi:94,
  AUTHOR    = "Ghilezan, Sylvia",
  TITLE     = "Application of Typed Lambda Calculi in the
              Untyped Lambda Calculus",
  BOOKTITLE = "Proceedings of the Third International Symposium
              on Logical Foundations of Computer Science (LFCS '94)",
  YEAR      = 1994,
  EDITOR    = "Nerode, A. and Matiyasevich, Yu.V.",
  PAGES     = "129--139",
  ADDRESS   = "St. Petersburg, Russia",
  MONTH     = jul,
  SERIES    = lncs,
  VOLUME    = 813
}


@PHDTHESIS{Gir:72,
  AUTHOR  = "Girard, Jean-Yves",
  TITLE   = "Interpr{\'e}tation fonctionelle et {\'e}limination 
            des coupures dans l'arithm{\'e}tique d'ordre sup{\'e}rieur",
  SCHOOL  = "Universit{\'e} Paris {VII}",
  YEAR    = 1972
}


@ARTICLE{Gir:87,
  AUTHOR  = "Girard, Jean-Yves",
  TITLE   = "Linear Logic",
  JOURNAL = tcs,
  YEAR    = 1987,
  VOLUME  = 50,
  PAGES   = "1--102"
}

@BOOK{Gir:Laf:Tay:89,
  AUTHOR    = "Girard, Jean-Yves and Lafont, Yves and Taylor, Paul",
  TITLE     = "Proofs and Types",
  PUBLISHER = cup,
  YEAR      = 1989,
  VOLUME    = 7,
  SERIES    = cttcs
}

@INPROCEEDINGS{Gla:Kha:94,
  AUTHOR    = "Glauert, J.R.W. and Khasidashvili, Z.",
  TITLE     = "Relative Normalization in Orthogonal Expression Reduction Systems",
  BOOKTITLE = "Proceedings of the 4th International Workshop on Conditional and
              Typed Term Rewriting Systems (CTRS '94)",
  YEAR      = 1994,
  EDITOR    = "Dershowitz, N.",
  PAGES     = "144-165",
  ADDRESS   = "Jerusalem, Israel",
  SERIES    = lncs,
  VOLUME    = 968
}

@INPROCEEDINGS{Gla:Kha:96a,
  AUTHOR    = "Glauert, J.R.W. and Khasidashvili, Z.",
  TITLE     = "Relative Normalization in Deterministic Residual Structures",
  BOOKTITLE = "Proceedings of the 19th International Colloquium on
              Trees in Algebras and Programming (CAAP '96)",
  MONTH     = apr,
  YEAR      = 1996,
  ADDRES    = "Link{\"o}ping, Sweden",
  NOTE      = "To appear"
}

@UNPUBLISHED{Gla:Kha:96b,
  AUTHOR = "Glauert, J.R.W. and Khasidashvili, Z.",
  TITLE  = "Minimal and Optimal Relative Normalization in 
           Orthogonal Expression Reduction Systems",
  YEAR   = 1996,
  NOTE   = "University of East Anglia"
}

@INPROCEEDINGS{Gon:Aba:Lev:92,
  AUTHOR    = "Gonthier, Georges and Abadi, Mart{\'\i}n and
              L{\'e}vy, Jean-Jacques ",
  TITLE     = "The geometry of optimal lambda reduction",
  BOOKTITLE = "Proceedings  of the 19th ACM
               Conference on Principles of
               Programming Languages (POPL '92)",
  YEAR      = 1992,
  PAGES     = "15--26"
}

@INPROCEEDINGS{Gon:Lev:Mel:92,
  AUTHOR    = "Gonthier, Georges and L{\'e}vy, Jean-Jacques and
              Melli{\`e}s, Paul-Andr{\'e}",
  TITLE     = "An abstract standardisation theorem",
  BOOKTITLE = "Proceedings of the seventh Annual IEEE Symposium on
              Logic in Computer Science (LICS '92)",
  PAGES     = "72--81",
  YEAR      = 1992,
  ADDRESS   = "Los Alamitos, California"
}

@INPROCEEDINGS{Gro:93,
  AUTHOR    = "Groote, Philippe de",
  TITLE     = "The Conservation Theorem revisited",
  BOOKTITLE = "Proceedings of the International Conference on
              Typed Lambda Calculi and Applications
              (TLCA '93)",
  YEAR      = 1993,
  EDITOR    = "Bezem, M. and Groote, J.F.",
  PAGES     = "163--178",
  ADDRESS   = "Utrecht, The Netherlands",
  MONTH     = mar,
  NOTE      = "Volume 664 of Lecture Notes in Computer Science"
}

@INPROCEEDINGS{Han:Pre:96,
  AUTHOR     ="Hanus, Michael and Prehofer, Christian",
  TITLE     = "Higher-Order Narrowing with Definitional Trees",
  BOOKTITLE = "Proceedings of the 7th International Conference on
              Rewriting Techniques and Applications (RTA '96)",
  YEAR      = 1996,
  EDITOR    = "Ganzinger, Harald",
  SERIES    = lncs,
  VOLUME    = 1103,
  PAGES     = "138--152",
  ADDRESS   = "New Brunswick, USA"
}
@ARTICLE{Hin:78,
  AUTHOR  = "Hindley, R.",
  TITLE   = "Reductions of Residuals are Finite",
  JOURNAL = tams,
  YEAR    = 1978,
  VOLUME  = 240,
  PAGES   = "345--361",
  MONTH   = jun
}


@BOOK{Hin:Sel:86,
  AUTHOR    = "Hindley, J. Roger and Seldin, Jonathan P.",
  TITLE     = "Introduction to Combinators and $\lambda$-Calculus",
  PUBLISHER = cup,
  YEAR      = 1986,
  VOLUME    = 1,
  SERIES    = lmsst
}

@ARTICLE{Hue:75,
  AUTHOR  = "Huet, G.P.",
  TITLE   = "A unification algorithm for typed 
            ${\overline \lambda}$-calculus",
  JOURNAL = tcs,
  YEAR    = 1975,
  VOLUME  = 1,
  PAGES   = "27--57"
}

@ARTICLE{Hue:80,
  AUTHOR  = "Huet, G{\'e}rard",
  TITLE   = "Confluent Reductions:
            Abstract Properties and Applications to Term Rewriting Systems",
  JOURNAL = jacm,
  YEAR    = 1980,
  VOLUME  = 27,
  NUMBER  = 4,
  PAGES   = "797--821",
  MONTH   = oct,
}

@ARTICLE{Hue:94,
  AUTHOR  = "Huet, G{\'e}rard",
  TITLE   = "Residual Theory in $\lambda$-calculus:
            a formal development",
  JOURNAL = jfp,
  YEAR    = 1994,
  VOLUME  = 4,
  NUMBER  = 3,
  PAGES   = "371--394"
}


@INCOLLECTION{Hue:Lev:91,
  AUTHOR    = "Huet, G{\'e}rard and L{\'e}vy, Jean-Jacques",
  TITLE     = "Computations in Orthogonal Rewriting Systems, {I} and {II}",
  BOOKTITLE = "Computational Logic:
              Essays in honor of Alan Robinson",
  PUBLISHER = mitp,
  YEAR      = 1991,
  EDITOR    = "Lassez, Jean-Louis and Plotkin, Gordon",
  PAGES     = "395--443",
  ADDRESS   = "Cambridge, Massachusetts"
}

@INCOLLECTION{Hue:Opp:80,
  AUTHOR    = "Huet, G{\'e}rard and Oppen, Derek C.",
  TITLE     = "Equations and Rewrite rules, a survey",
  BOOKTITLE = "Formal Language Theory,
              Perspectives and Open Problems",
  PUBLISHER = ap,
  YEAR      = 1980,
  EDITOR    = "Book, R.V.",
  PAGES     = "349--405"
}


@TECHREPORT{Hyl:73,
  AUTHOR      = "Hyland, J.M.E.",
  TITLE       = "A simple proof of the {C}hurch-{R}osser theorem",
  INSTITUTION = "Oxford University",
  YEAR        = 1973
}


@PHDTHESIS{Joi:93,
  AUTHOR  = "Joinet, J.-B.",
  TITLE   = "Etude de la normalisation du calcul des
            s{\'e}quents classique {\`a} travers la
            logique lin{\'e}aire",
  SCHOOL  = "Universit{\'e} Paris {VII}",
  YEAR    = 1993
}

@INPROCEEDINGS{Jou:Oka:91,
  AUTHOR    = "Jouannaud, Jean-Pierre and Okada, Mitsuhiro",
  TITLE     = "A Computational Model for Executable Higher-Order
              Algebraic Specification Languages",
  BOOKTITLE = "Proceedings of the sixth annual IEEE Symposium on
              Logic in Computer Science (LICS '91)",
  YEAR      = 1991,
  PAGES     = "350--361",
  ADDRESS   = "Amsterdam",
  MONTH     = jul,
}

@INPROCEEDINGS{Kah:93,
  AUTHOR    = "Kahrs, Stefan",
  TITLE     = "Compilation of Combinatory Reduction Systems",
  BOOKTITLE = "Proceedings of the First International Workshop
              on Higher-Order Algebra, Logic and Term Rewriting
              (HOA '93)",
  YEAR      = 1994,
  EDITOR    = "Heering, J. and Meinke, K. and
              M{\"o}ller, B. and Nipkow, T.",
  SERIES    = lncs,
  VOLUME    = 816,
  PAGES     = "169--188",
  ADDRESS   = "Amsterdam, The Netherlands"
}

@INPROCEEDINGS{Kah:95,
  AUTHOR    = "Kahrs, Stefan",
  TITLE     = "Towards a domain theory for termination proofs",
  BOOKTITLE = "Proceedings of the 6th International Conference on
              Rewriting Techniques and Applications (RTA '95)",
  YEAR      = 1995,
  EDITOR    = "Hsiang, Jieh",
  PAGES     = "241--255",
  ADDRESS   = "Kaiserslautern, Germany",
  MONTH     = apr,
  VOLUME    = 941,
  SERIES    = lncs
}

@TECHREPORT{Ken:92,
  AUTHOR      = "Kennaway, J.R.",
  TITLE       = "On transfinite abstract reduction systems",
  INSTITUTION = "CWI",
  NUMBER      = "CS-R9205",
  MONTH       = jan,
  YEAR        = 1992
}

@INPROCEEDINGS{Kha:90,
  AUTHOR    = "Khasidashvili, Z.O.",
  TITLE     = "Expression {R}eduction {S}ystems",
  BOOKTITLE = "Proceedings of I. Vekua Institute of Applied
              Mathematics",
  YEAR      = 1990,
  VOLUME    = 36,
  PAGES     = "200--220",
  ADDRESS   = "Tblisi"
}

@TECHREPORT{Kha:92,
  AUTHOR      = "Khasidashvili, Z.O.",
  TITLE       = "The {C}hurch-{R}osser theorem in orthogonal
                Combinatory Reduction Systems",
  INSTITUTION = "INRIA Rocqencourt",
  NUMBER      = 1825,
  YEAR        = 1992,
  ADDRESS     = "France"
}


@INPROCEEDINGS{Kha:93,
  AUTHOR    = "Khasidashvili, Zurab",
  TITLE     = "Optimal Normalization in Orthogonal
              Term Rewriting Systems",
  BOOKTITLE = "Proceedings of the Fifth International Conference
              on Rewriting Techniques and Applications (RTA '93)",
  YEAR      = 1993,
  EDITOR    = "Kirchner, Claude",
  PAGES     = "243--258",
  ADDRESS   = "Montreal, Canada",
  MONTH     = jun,
  SERIES    = lncs,
  NUMBER    = 690
}

@INPROCEEDINGS{Kha:94,
  AUTHOR    = "Khasidashvili, Zurab",
  TITLE     = "The longest perpetual reductions in
              orthogonal Expression Reduction Systems",
  BOOKTITLE = "Proceedings of the Third International Symposium
              on Logical Foundations of Computer Science (LFCS '94)",
  YEAR      = 1994,
  EDITOR    = "Nerode, A. and Matiyasevich, Yu.V.",
  PAGES     = "191--203",
  ADDRESS   = "St. Petersburg, Russia",
  MONTH     = jul,
  SERIES    = lncs,
  NUMBER    = 813
}

@ARTICLE{Kha:Oos:95,
  AUTHOR  = "Khasidashvili, Z. and Oostrom, V. van",
  TITLE   = "Context-sensitive Conditional Expression Reduction
            Systems",
  JOURNAL = "Elsevier, Electronic Notes in Theoretical Computer Science",
  YEAR    = 1995,
  VOLUME  = 2,
  NOTE    = "Available at http://www.elsevier/nl/mcs/tcs/pc/volume2.htm"
}

@BOOK{Klo:80,
  AUTHOR    = "Klop, J.W.",
  TITLE     = "Combinatory Reduction Systems",
  PUBLISHER = "CWI",
  YEAR      = 1980,
  VOLUME    = 127,
  SERIES    = mct,
  ADDRESS   = "Amsterdam", 
  NOTE      = "PhD Thesis"
}

@INCOLLECTION{Klo:92,
  AUTHOR    = "Klop, J.W.",
  TITLE     = "Term rewriting systems",
  BOOKTITLE = "Handbook of Logic in Computer Science",
  PUBLISHER = oup,
  YEAR      = 1992,
  EDITOR    = "Abramsky, S. and Gabbay, Dov M. and Maibaum, T.S.E.",
  PAGES     = "1--116",
  ADDRESS   = "New York",
  VOLUME    = 2,
}

@ARTICLE{Klo:Oos:Raa:93,
  AUTHOR  = "Klop, J.W. and Oostrom, V. van and Raamsdonk, F. van ",
  TITLE   = "Combinatory Reduction Systems: introduction and survey",
  JOURNAL = tcs,
  YEAR    = 1993,
  VOLUME  = 121,
  PAGES   = "279--308",
  NOTE    = "Special issue in honour of {C}orrado {B}{\"o}hm"
}


@ARTICLE{Klo:Vrij:89,
  AUTHOR  = "Klop, J.W. and Vrijer, R.C. de",
  TITLE   = "Unique Normal Forms for Lambda Calculus
            with Surjective Pairing",
  JOURNAL = ic,
  YEAR    = 1989,
  VOLUME  = 80,
  PAGES   = "97--113",
}

@BOOK{Kri:93,
  AUTHOR    = "Krivine, J.L.",
  TITLE     = "Lambda-Calculus, Types and Models",
  PUBLISHER = m,
  YEAR      = 1993,
  ADDRESS   = "Paris, France"
}


@INPROCEEDINGS{Laf:90,
  AUTHOR    = "Lafont, Yves",
  TITLE     = "Interaction Nets",
  BOOKTITLE = "Proceedings of the 17th ACM Symposium on
              Principles of Programming Languages (POPL '90)",
  YEAR      = 1990,
  PAGES     = "95--108",
  ADDRESS   = "San Francisco, USA",
  MONTH     = jan
}

@INPROCEEDINGS{Lam:90,
  AUTHOR     = "Lamping, John",
  TITLE      = "An Algorithm for Optimal Lambda Calculus Reduction",
  BOOKTITLE  = "Proceedings of the 17th ACM
               Conference on Principles of 
               Programming Languages (POPL '90)",
  YEAR       = 1990,
  PAGES      = "16--30",
 ADDRESS     = "San Francisco, USA",
  MONTH      = jan
}



@PHDTHESIS{Lan:93,
  AUTHOR  = "Laneve, Cosimo",
  TITLE   = "Optimality and Concurrency in
            Interaction Systems",
  SCHOOL  = "Universit{\`a} di Pisa",
  YEAR    = 1993,
  ADDRESS = "Pisa, Italy",
  MONTH   = mar
}


@PHDTHESIS{Lev:78,
  AUTHOR  = "L{\'e}vy, Jean-Jacques",
  TITLE   = "R{\'e}ductions correctes et optimales
            dans le lambda-calcul",
  SCHOOL  = "Universit{\'e} de Paris VII",
  YEAR    = 1978
}

@UNPUBLISHED{Loa:95,
  AUTHOR  = "Loader, R.",
  TITLE   = "Normalisation by Translation",
  YEAR    = "1995",
  MONTH   = "April",
  NOTE    = "Note distributed on the `types' mailing list"
}

@INPROCEEDINGS{Lys:Pir:95,
  AUTHOR    = "Lysne, Olav and Piris, Javier",
  TITLE     = "A Termination Ordering for Higher-Order 
               Rewrite Systems",
  BOOKTITLE = "Proceedings of the 6th International Conference on
              Rewriting Techniques and Applications (RTA '95)",
  YEAR      = 1995,
  EDITOR    = "Hsiang, Jieh",
  PAGES     = "26--40",
  SERIES    = lncs,
  VOLUME    = "914",
  ADDRESS   = "Kaiserslautern, Germany",
  MONTH     = apr

}


@TECHREPORT{May:Nip:94,
  AUTHOR      = "Mayr, Richard and Nipkow, Tobias",
  TITLE       = "Higher-Order Rewrite Systems and their Confluence",
  INSTITUTION = "Technische Universit{\"a}t M{\"u}nchen",
  NUMBER      = "TUM-I9433",
  MONTH       = aug,
  YEAR        = 1994
}

@PHDTHESIS{Mel:96,
  AUTHOR  = "Melli{\`e}s, Paul-Andr{\'e}",
  TITLE   = "Description Abstraite des Syst{\`e}mes de R{\'e}{\'e}criture",
  SCHOOL  = "Universit{\'e} de Paris VII",
  YEAR    = "1996",
  NOTE    = "To appear"
}

@PHDTHESIS{Meu:94,
  AUTHOR  = "Meulen, Emma A. van der",
  TITLE   = "Incremental Rewriting",
  SCHOOL  = "Universiteit van Amsterdam",
  YEAR    = 1994,
  MONTH   = jan, 
}

@ARTICLE{Mil:91,
  AUTHOR  = "Miller, Dale",
  TITLE   = "A logic programming language with lambda-abstraction,
            function variables, and simple unification",
  JOURNAL = jlc,
  YEAR    = 1991,
  VOLUME  = 1,
  NUMBER  = 4,
  PAGES   = "497--536"
}

@PHDTHESIS{Ned:73,
  AUTHOR  = "Nederpelt, R.P.",
  TITLE   = "Strong Normalization in a Typed Lambda Calculus
            with Lambda Structured Types",
  SCHOOL  = "Technische Hogeschool Eindhoven",
  YEAR    = 1973,
  MONTH   = jun
}

@BOOK{Ned:Geu:Vri:94,
  EDITOR    = "Nederpelt, R.P. and Geuvers, J.H. and 
              Vrijer, R.C. de",
  TITLE     = "Selected Papers on Automath",
  PUBLISHER = es,
  YEAR      = 1994,
  VOLUME    = 133,
  SERIES    = slfm
}



@ARTICLE{New:42,
  AUTHOR  = "Newman, M.H.A",
  TITLE   = "On theories with a combinatorial definition
            of ``equivalence''",
  JOURNAL = am,
  YEAR    = 1942,
  VOLUME  = 43,
  NUMBER  = 2,
  PAGES   = "223--243",
  MONTH   = apr
}

@INPROCEEDINGS{Nip:91,
  AUTHOR    = "Nipkow, Tobias",
  TITLE     = "Higher-order Critical Pairs",
  BOOKTITLE = "Proceedings of the sixth annual IEEE Symposium on
              Logic in Computer Science (LICS '91)",
  YEAR      = 1991,
  PAGES     = "342--349",
  ADDRESS   = "Amsterdam, The Netherlands",
  MONTH     = jul,
}

@INPROCEEDINGS{Nip:93,
  AUTHOR    = "Nipkow, Tobias",
  TITLE     = "Orthogonal Higher-order Rewrite Systems 
              are confluent",
  BOOKTITLE = "Proceedings of the International Conference on
              Typed Lambda Calculi and Applications
              (TLCA '93)",
  YEAR      = 1993,
  EDITOR    = "Bezem, M. and Groote, J.F.",
  PAGES     = "306--317",
  ADDRESS   = "Utrecht, The Netherlands",
  MONTH     = mar,
  SERIES    = lncs,
  VOLUME    = 664
}

@INPROCEEDINGS{Nip:93:b,
  AUTHOR    = "Nipkow, Tobias",
  TITLE     = "Functional Unification of Higher-Order Patterns",
  BOOKTITLE = "Proceedings of the eigth annual IEEE Symposium on
              Logic in Computer Science (LICS '93)",
  YEAR      = 1993,
  PAGES     = "64--74",
  ADDRESS   = "Montreal, Canada",
  MONTH     = jun,
}

@INPROCEEDINGS{Nip:96,
  AUTHOR    = "Nipkow, Tobias",
  TITLE     = "More {Church-Rosser} Proofs
                (in {Isabelle/HOL})",
  BOOKTITLE = "Proceedings of the 13th International Conference on
              Automated Deduction (CADE '96)",
  YEAR      = 1996,
  ADDRES    = "New Jersey",
  NOTE      = "To appear"
}

@BOOK{OD:77,
  AUTHOR    = "O'Donnell, Michael J.",
  TITLE     = "Computing in Systems Described by Equations",
  PUBLISHER = sv,
  YEAR      = 1977,
  VOLUME    = 58,
  SERIES    = lncs,
}


@PHDTHESIS{Oos:94,
  AUTHOR  = "Oostrom, Vincent van",
  TITLE   = "Confluence for Abstract and
             Higher-Order Rewriting",
  SCHOOL  = "Vrije Universiteit",
  YEAR    = 1994,
  ADDRESS = "Amsterdam",
  MONTH   = mar,
  NOTE    = "Available at \verb+http://www.cs.vu.nl/~oostrom+"
}

@INPROCEEDINGS{Oos:96,
  AUTHOR    = "Oostrom, Vincent van",
  TITLE     = "Development Closed Critical Pairs",
  BOOKTITLE = "Proceedings of the Second International Workshop
              on Higher-Order Algebra, Logic and Term Rewriting
              (HOA '95)",
  YEAR      = 1996,
  EDITOR    = "Dowek, G. and Heering, J. and Meinke, K. and
              M{\"o}ller, B.",
  SERIES    = lncs,
  VOLUME    = 1074,
  PAGES     = "185--200",
  ADDRESS   = "Paderborn, Germany"
}

@INPROCEEDINGS{Oos:96:b,
  AUTHOR     ="Oostrom, Vincent van",
  TITLE     = "Higher-Order Families",
  BOOKTITLE = "Proceedings of the 7th International Conference on
              Rewriting Techniques and Applications (RTA '96)",
  YEAR      = 1996,
  EDITOR    = "Ganzinger, Harald",
  SERIES    = lncs,
  VOLUME    = 1103,
  PAGES     = "392-407",
  ADDRESS   = "New Brunswick, USA"
}

@MISC{Oos:96:c,
  AUTHOR = "Oostrom, Vincent van",
  TITLE  = "Personal communication",
  YEAR   = 1996
}

@INPROCEEDINGS{Oos:Raa:93a,
  AUTHOR    = "Oostrom, Vincent van and Raamsdonk, Femke van",
  TITLE     = "Comparing Combinatory Reduction Systems and
               Higher-order Rewrite Systems",
  BOOKTITLE = "Proceedings of the First International Workshop
              on Higher-Order Algebra, Logic and Term Rewriting
              (HOA '93)",
  YEAR      = 1994,
  EDITOR    = "Heering, J. and Meinke, K. and
              M{\"o}ller, B. and Nipkow, T.",
  SERIES    = lncs,
  VOLUME    = 816,
  ADDRESS   = "Amsterdam"
}

@TECHREPORT{Oos:Raa:93b,
  AUTHOR      = "Oostrom, Vincent van and Raamsdonk, Femke van",
  TITLE       = "Comparing Combinatory Reduction Systems and
                Higher-order Rewrite Systems",
  INSTITUTION = "CWI",
  NUMBER      = "CS-R9361",
  MONTH       = sep,
  YEAR        = 1993
}


@INPROCEEDINGS{Oos:Raa:94,
  AUTHOR    = "Oostrom, Vincent van and Raamsdonk, Femke van",
  TITLE     = "Weak orthogonality implies confluence:
              the higher-order case",
  BOOKTITLE = "Proceedings of the Third International Symposium
              on Logical Foundations of Computer Science (LFCS '94)",
  YEAR      = 1994,
  EDITOR    = "Nerode, A. and Matiyasevich, Yu.V.",
  PAGES     = "379--392",
  ADDRESS   = "St. Petersburg",
  MONTH     = jul,
  SERIES    = lncs,
  VOLUME    = 813
}

@TECHREPORT{Oos:95,
  AUTHOR      = "Oostrom, Vincent van and Raamsdonk, Femke van",
  TITLE       = "Weak orthogonality implies confluence:
                the higher-order case",
  INSTITUTION = "CWI",
  NUMBER      = "CS-R9501",
  MONTH       = jan,
  YEAR        = 1995
}

@INPROCEEDINGS{Par:90,
  AUTHOR    = "Parigot, Michel",
  TITLE     = "Internal Labellings in Lambda-Calculus",
  BOOKTITLE = "Proceedings of the 15th Symposium on
              Mathematical Foundations of Computer Science (MFCS '90)",
  YEAR      = 1990,
  EDITOR    = "Rovan, B.",
  PAGES     = "439--445",
  ADDRESS   = "Bansk{\'a} Bystrica, Czechoslovakia",
  MONTH     = aug,
  SERIES    = lncs,
  VOLUME    = 452
}


@TECHREPORT{Pkh:77,
  AUTHOR      = "Pkhakadze, Sh.",
  TITLE       = "Some problems of the Notation Theory",
  INSTITUTION = "I. Vekua Institute of Applied Mathematics",
  YEAR        = 1977,
  NOTE        = "In Russian",
  ADDRESS     = "Tblisi, Georgia"
}


@ARTICLE{Plo:77,
  AUTHOR  = "Plotkin, G.D.",
  TITLE   = "{LCF} considered as a programming language",
  JOURNAL = tcs,
  YEAR    = 1977,
  VOLUME  = 5,
  PAGES   = "223--255"
}


@TECHREPORT{Plo:81,
  AUTHOR      = "Plotkin, Gordon D.",
  TITLE       = "A structured approach to operational semantics",
  INSTITUTION = "Aarhus University",
  NUMBER      = "DAIMI FN-19",
  MONTH       = sep,
  YEAR        = 1981,
}

@INPROCEEDINGS{Pol:93,
  AUTHOR    = "Pol, J.C. van de",
  TITLE     = "Termination Proofs for Higher-Order Rewrite Systems",
  BOOKTITLE = "Proceedings of the First International Workshop
              on Higher-Order Algebra, Logic and Term Rewriting
              (HOA '93)",
  YEAR      = 1994,
  EDITOR    = "Heering, J. and Meinke, K. and
              M{\"o}ller, B. and Nipkow, T.",
  SERIES    = lncs,
  VOLUME    = 816,
  PAGES     = "305--325",
  ADDRESS   = "Amsterdam, The Netherlands"
}

@INPROCEEDINGS{Pol:Sch:95,
  AUTHOR    = "Pol, Jaco van de and Schwichtenberg, Helmut ",
  TITLE     = "Strict Functionals for Termination Proofs",
  BOOKTITLE = "Proceedings of the Second International Conference on
              Typed Lambda Calculi and Applications (TLCA '95)",
  YEAR      = 1995,
  EDITOR    = "Dezani-Ciancaglini, M. and Plotkin, G.",
  SERIES    = lncs,
  NUMBER    = 902,
  PAGES     = "350--364",
  ADDRESS   = "Edinburgh"
}

@INPROCEEDINGS{Pol:96,
  AUTHOR    = "Pol, Jaco van de",
  TITLE     = "Two {\em different} strong normalization proofs?",
  BOOKTITLE = "Proceedings of the Second International Workshop
              on Higher-Order Algebra, Logic and Term Rewriting
              (HOA '95)",
  YEAR      = 1996,
  EDITOR    = "Dowek, G. and Heering, J. and Meinke, K. and
              M{\"o}ller, B.",
  SERIES    = lncs,
  VOLUME    = 1074,
  PAGES     = "201--220",
  ADDRESS   = "Paderborn, Germany"
}



@PHDTHESIS{Pre:95,
  AUTHOR  = "Prehofer, Christian",
  TITLE   = "Solving Higher-Order Equations:
            From Logic to Programming",
  SCHOOL  = "Technische Universit{\"a}t M{\"u}nchen",
  YEAR    = 1995
}

@UNPUBLISHED{Raa:92,
  AUTHOR = "Raamsdonk, Femke van",
  TITLE  = "Representations of $\lambda$-terms as Proof Nets",
  YEAR   = 1992,
  NOTE   = "Master's Thesis"
}

@INPROCEEDINGS{Raa:93,
  AUTHOR    = "Raamsdonk, Femke van",
  TITLE     = "Confluence and Superdevelopments",
  BOOKTITLE = "Proceedings of the 5th International Conference on
              Rewriting Techniques and Applications (RTA '93)",
  YEAR      = 1993,
  EDITOR    = "Kirchner, Claude",
  PAGES     = "168--182",
  ADDRESS   = "Montreal, Canada",
  MONTH     = jun,
  NOTE      = "Volume 690 of Lecture Notes in Computer Science"
}

@PHDTHESIS{Raa:96,
  AUTHOR  = "Raamsdonk, Femke van",
  TITLE   = "Confluence and Normalisation for 
            Higher-Order Rewriting",
  SCHOOL  = "Vrije Universiteit",
  YEAR    = 1996,
  ADDRESS = "Amsterdam",
  MONTH   = may,
  NOTE    = "Available at \verb+http://www.cwi.nl/~femke+"
}

@TECHREPORT{Raa:Sev:95,
  AUTHOR      = "Raamsdonk, F. van and Severi, P.",
  TITLE       = "On Normalisation",
  INSTITUTION = "CWI",
  NUMBER      = "CS-R9545",
  MONTH       = jun,
  YEAR        = 1995
}

@PHDTHESIS{Reg:92,
  AUTHOR  = "R{\'e}gnier, Laurent",
  TITLE   = "Lambda-calcul et r{\'e}seaux",
  SCHOOL  = "Universit{\'e} Paris {VII}",
  YEAR    = 1992
}

@INPROCEEDINGS{Rey:74,
  AUTHOR    = "Reynolds, John C.",
  TITLE     = "Towards a theory of type structure",
  BOOKTITLE = "Proceedings of the `Colloque sur la
              Programmation'",
  YEAR      = 1974,
  SERIES    = lncs,
  NUMBER    = 19,
  PAGES     = "408--425",
  ADDRESS   = "Paris, France"
}

@TECHREPORT{Roo:Ter:93,
  AUTHOR      = "Roorda, Dirk and Terlouw, Jan",
  TITLE       = "$\lambda$-calculus",
  INSTITUTION = "Rijksuniversiteit Groningen",
  YEAR        = 1993,
  NOTE        = "Coursnotes"
}


@PHDTHESIS{Ros:96,
  AUTHOR  = "Rose, Kristoffer H.",
  TITLE   = "Operational Reduction Models
            for Functional Programming Languages",
  SCHOOL  = "University of Copenhagen",
  YEAR    = 1996
}

@ARTICLE{Ros:73,
  AUTHOR  = "Rosen, Barry K.",
  TITLE   = "Tree-Manipulating Systems and
            {C}hurch-{R}osser Theorems",
  JOURNAL = jacm,
  YEAR    = 1973,
  VOLUME  = 20,
  NUMBER  = 1,
  PAGES   = "160--187",
  MONTH   = jan
}

@INPROCEEDINGS{Ros:82,
  AUTHOR    = "Rosser, J. Barkley",
  TITLE     = "Highlights of the History of the
              Lambda-calculus",
  BOOKTITLE = "Proceedings of the ACM symposium on
              {LISP} and Functional Programming",
  YEAR      = 1982,
  PAGES     = "216--225",
  ADDRESS   = "New York"
}

@ARTICLE{Sch:24,
  AUTHOR  = "Sch{\"o}nfinkel, M.",
  TITLE   = "{\"U}ber die {B}austeine der mathematischen {L}ogik",
  JOURNAL = ma,
  YEAR    = 1924,
  VOLUME  = 92,
  PAGES   = "305--316"
}



@PHDTHESIS{Sch:65,
  AUTHOR  = "Schroer, D.E.",
  TITLE   = "The Church-Rosser Theorem",
  SCHOOL  = "Cornell University",
  YEAR    = 1965
}


@PHDTHESIS{Sch:94,
  AUTHOR  = "Schellinx, H.A.J.M.",
  TITLE   = "The Noble Art of Linear Decorating",
  SCHOOL  = "Universiteit van Amsterdam",
  YEAR    = 1994,
  MONTH   = feb,
}


@INPROCEEDINGS{Sek:Ram:90,
  AUTHOR    = "Sekar, R.C. and Ramakrishnan, I.V.",
  TITLE     = "Programming in Equational Logic:
              Beyond strong sequentiality",
  BOOKTITLE = "Proceedings of the seventh International
              Symposium on Logic in Computer Science (LICS '90)",
  YEAR      = 1990,
  PAGES     = "230--241"
}

@PHDTHESIS{Spr:95,
  AUTHOR  = "Springintveld, Jan",
  TITLE   = "Algorithms for Type Theory",
  SCHOOL  = "Universiteit Utrecht",
  YEAR    = 1995,
  MONTH   = may
}

@BOOK{Sten:72,
  AUTHOR    = "Stenlund, S.",
  TITLE     = "Combinators, $\lambda$-terms, and Proof Theory",
  PUBLISHER = "Reidel",
  YEAR      = 1972
}


@INPROCEEDINGS{Tak:93,
  AUTHOR    = "Takahashi, Masako",
  TITLE     = "$\lambda$-Calculi with Conditional Rules",
  BOOKTITLE = "Proceedings of the International Conference on
              Typed Lambda Calculi and Applications
              (TLCA '93)",
  YEAR      = 1993,
  EDITOR    = "Bezem, M. and Groote, J.F.",
  PAGES     = "406--417",
  ADDRESS   = "Utrecht, The Netherlands",
  MONTH     = mar,
  VOLUME    = 664,
  SERIES    = lncs
}

@ARTICLE{Tai:67,
  AUTHOR  = "Tait, W.W.",
  TITLE   = "Intensional interpretation of functionals of finite type {I}",
  JOURNAL = jsl,
  YEAR    = 1967,
  VOLUME  = 32,
  PAGES   = "198--212",
}
 

@ARTICLE{Tak:95,
  AUTHOR  = "Takahashi, Masako",
  TITLE   = "Parallel Reductions in $\lambda$--Calculus",
  JOURNAL = ic,
  YEAR    = 1995,
  VOLUME  = 118,
  PAGES   = "120--127",
}

@ARTICLE{Ter:95,
  AUTHOR  = "Terlouw, Jan",
  TITLE   = "Strong normalization in type systems:
            a model theoretic approach",
  JOURNAL = apal,
  YEAR    = 1995,
  VOLUME  = 73,
  PAGES   = "53--78"
}


@ARTICLE{Vrij:85,
  AUTHOR  = "Vrijer, Roel de",
  TITLE   = "A direct proof of the finite developments theorem",
  JOURNAL = jsl,
  YEAR    = 1985,
  VOLUME  = 50,
  NUMBER  = 2,
  PAGES   = "339--343",
  MONTH   = jun
}

@PHDTHESIS{Vrij:87,
  AUTHOR  = "Vrijer, Roel de",
  TITLE   = "Surjective Pairing and Strong Normalization:
            Two Themes in Lambda Calculus",
  SCHOOL  = "Universiteit van Amsterdam",
  YEAR    = 1987,
  MONTH   = jan
}

@ARTICLE{Vrij:87:b,
  AUTHOR  = "Vrijer, Roel de",
  TITLE   = "Exactly estimating functionals and strong normalization",
  JOURNAL = "Proceedings of the Koninklijke Nederlandse Akademie van
            Wetenschappen",
  YEAR    = 1987,
  VOLUME  = 90,
  NUMBER  = 4,
  MONTH   = dec
}

@PHDTHESIS{Wad:71, 
  AUTHOR  = "Wadsworth, C.P.",
  TITLE   = "Semantics and Pragmatics of the Lambda-Calculus",
  SCHOOL  = "Oxford University",
  YEAR    = 1971
}

@INPROCEEDINGS{Wol:91,
  AUTHOR    = "Wolfram, D.A.",
  TITLE     = "Rewriting, and Equational Unification:
              the Higher-Order Cases",
  BOOKTITLE = "Proceedings of the 4th International Conference on
              Rewriting Techniques and Applications (RTA '91)",
  YEAR      = 1991,
  ADRESS    = "Como, Italy"
}


@BOOK{Wol:93,
  AUTHOR     = "Wolfram, D.A.",
  TITLE      = "The Clausal Theory of Types",
  PUBLISHER  = cup,
  YEAR       = 1993,
  SERIES     = cttcs,
  VOLUME     = 21
}