------bibliography file follows this line:----------------------------
The "preamble" command defines macros that will be available to use in the
text fields of each entry.  These are intended to be used in the format:

  {\bibXXX{YYY}}

This will make BibTeX see the text YYY as a single character, and will
have the TeX macro \bibXXX be applied to YYY if it appears in a document.

@preamble{ "\newcommand{\bibnoop}[1]{}"
           # "\newcommand{\bibsingleletter}[1]{#1}" }

=============
Organizations
=============

@string{IEEE = "Institute of Electrical and Electronic Engineers"}
@string{IEEE = "IEEE"}
@string{ACM = "ACM"}
@string{IEEECS = "The IEEE Computer Society"}
@string(IFIP = {International Federation for Information Processing})
@string{IFIP = "IFIP"}

==========
Publishers
==========

@string{IEEECSP = "The IEEE Computer Society Press"}
@string{SV = "Springer-Verlag"}
@string{CUP = "Cambridge University Press"}
@string{OUP = "Oxford University Press"}
@string{MIT = "MIT Press"}

========
Journals
========

@string{TCS = "Theoretical Computer Science"}
@string{MSCS = "Mathematical Structures in Computer Science"}
@string(JACM = "Journal of the ACM")

======
Series
======

@string(LNCS = "Lecture Notes in Computer Science")
@string(LNCS = "LNCS")

=======
Authors
=======

@TechReport{[Acz],
	author = "P. Aczel",
	title = "A General {Church}-{Rosser} Theorem",
	institution = "University of Manchester",
	year = 1978,
}

@InProceedings{[Ant],
	author = "S. Antoy and R. Echahed and M. Hanus",
	title = "A Needed Narrowing Strategy",
	booktitle = "$21^{st}$ ACM Symposium on Principles of Programming Languages, POPL'94",
	publisher = ACM,
	year = 1994,
	pages = "268--279",
}

@Article{[AnMi],
	author = "S. Antoy and A. Middeldorp",
	title = "A Sequential Reduction Strategy",
	journal = TCS,
	volume = 165,
	number = 1,
	pages = "75--95",
	year = 1996,
}

@Article{[AL],
	author = "A. Asperti and C. Laneve",
	title = "Interaction {Systems} {I}: The Theory of Optimal Reductions",
	journal = MSCS,
	volume = 11, 
	publisher = CUP,
	pages = "1-48",
	year = 1993,
}

@TechReport{[BBKV],
	author = "H. P. Barendregt and J. Bergstra and J. W. Klop and H. Volken",
	title = "Degrees, Reductions and Representability in the $\lambda$-Calculus",
	number = 22,
	institution = "University of Utrecht",
	year = 1976,
}

@Book{[Bar],
	author = "H. P. Barendregt",
	title = "The Lambda Calculus, its Syntax and Semantics",
	publisher = "North-Holland",
	year = 1984,
}

@Article{[B.K.K.S.],
	author = "H. P. Barendregt and J. R. Kennaway and J. W. Klop and M. R. Sleep",
 	title = "Needed Reduction and Spine Strategies for the Lambda Calculus",
	journal = "Information and Computation",
	volume = 75,
	number = 3,
	pages = "191--231",
	year = 1987,
}

@Article{[B.L.],
	author = "G. Berry and J.-J. L\'evy",
	title = "Minimal and Optimal Computations of Recursive Programs",
	journal = JACM,
	volume = 26,
	pages = "148--175",
	year = 1979,
}

@InCollection{[Bou],
	author = "G. Boudol",
	title = "Computational Semantics of Term Rewriting Systems",
	booktitle = "Algebraic Methods in Semantics",
	editor = "M. Nivat and J. C. Reynolds",
	publisher = CUP,
	pages = "169--236",
	year = 1985,
}

@Book{[C.F.],
	author = "H. B. Curry and R. Feys",
	title = "Combinatory Logic",
	volume = 1,
	publisher = "North-Holland",
	year = 1958,
}

@InCollection{[D.J.]}
	author = "N. Dershowitz and J.-P. Jouannaud",
	title = "Rewrite Systems",
	editor = "J. van Leeuwen",
	booktitle = "Handbook of  Theoretical Computer Science",
	chapter = 6,
	volume = "B",
	pages = "243--320",
	year = 1990,
}

@InProceedings{[Gar],
	author = "P. Gardner",
	title = "Discovering Needed Reductions Using Type Theory",
	booktitle = "$2^{nd}$ International Symposium on Theoretical Aspects of Computer Software, TACS'94",
	series = "LNCS",
	volume = 789,
	publisher = SV,
	editor = "M. Hagiya and J. C. Mitchell",
	pages = "555--574",
	year = 1994,
}

@InProceedings{[ctrs],
	author = "J. R. W. Glauert and Z.  Khasidashvili",
	title = "On Relative Normalization in Orthogonal Expression Reduction Systems",
	booktitle = "$4^{th}$ International Workshop on Conditional (and Typed) Term Rewriting Systems, CTRS'94",
	series = LNCS,
	volume = 968,
	publisher = SV,
	editor = "N. Dershowitz and N. Lindenstrauss",
	pages = "144--165",
	year = 1994,
}


@TechReport{[morn],
	author = "J. R. W. Glauert and Z.  Khasidashvili",
	title = "Minimal and Optimal Relative Normalization in Expression Reduction Systems",
	number = "SYS-C94-06", 
	institution = "UEA, Norwich, UK",
	year = 1994,
}

@InProceedings{[rndrs],
	author = "J. R. W. Glauert and Z.  Khasidashvili",
	title = "Relative Normalization in Deterministic Residual Structures",
	booktitle = "$19^{th}$ International Colloquium on Trees in Algebra and Programming, CAAP'96",
	publisher = SV,
	series = LNCS,
	volume = 1059,
	editor = "H. Kirchner",
	pages = "180--195",
	year = 1996,
}

@InProceedings{[fsttcs],
	author = "J. R. W. Glauert and Z.  Khasidashvili",
	title = "Minimal Relative Normalization in Orthogonal Expression Reduction Systems",
	booktitle = "$16^{th}$ International Conference on Foundations of Software Technology and Theoretical Computer Science, FST\&TCS'96",
	publisger = SV,
	series = LNCS,
	volume = 1180,
	editor = "V. Chandru",
	pages = "238--249",
	year = 1996,
}

@InProceedings{[GLM],
	author = "G. Gonthier and J.-J. L\'evy and P.-A. Melli\`es",
	title = "An Abstract Standardisation Theorem",
	booktitle = "$7^{th}$ Annual IEEE Symposium on Logic in Computer Science, LICS'92",
	publisher = IEEECSP,
	pages = "72--81",
	year = 1992,
}

@InProceedings{[HP96],
	author = "M. Hanus and C. Prehofer",
	title = "Higher-Order Narrowing with Definitional Trees",
	booktitle = "$7^{th}$ International Conference on Rewriting Techniques and Applications, RTA'96",
	publisher = SV,
	series = LNCS,
	volume = 1103,
	editor = "H. Ganzinger",
	pages = "138--152",
	year = 1996,
}

@InCollection{[H.L.],
	author = "G. Huet and J.-J. L\'evy",
	title = "Computations in Orthogonal Rewriting Systems",
	booktitle = "Computational Logic, Essays in Honor of Alan Robinson",
	editor = "J.-L. Lassez and G. Plotkin",
	publisher = MIT,
	year = 1991,
}

@Article{[Kenn],
	author = "J. R. Kennaway",
	title = "Sequential Evaluation Strategies for Parallel-Or and Related Reduction Systems",
	journal = "Annals of Pure and Applied Logic",
	volume = 43,
	pages = "31--56",
	year = 1989,
}

@TechReport{[K.S.],
	author = "J. R. Kennaway and M. R. Sleep",
	title = "Neededness is Hypernormalizing in Regular Combinatory Reduction Systems",
	institution = "UEA, Norwich, UK",
	year = 1989,
}

@Article{[K-tra],
	author = "J. R. Kennaway and J. W. Klop and M. R. Sleep and F.-J. de Vries",
	title = "Transfinite Reductions in Orthogonal Term Rewriting",
	journal = "Information and Computation",
	volume = 119,
	number = 1,
	pages = "18--38",
	year =1995,
}


@InProceedings{[colog],
	author = "Z. Khasidashvili",
	title = "$\beta$-Reductions and $\beta$-Developments of $\lambda$-terms with the Least Number of Steps",
	booktitle = "International Conference on Computer Logic, COLOG'88",
	publisher = SV,
	series = LNCS,
	volume = 417,
	editor = "P. Martin-{L\"of} and G. Mints",
	year = 1990,
	pages = "105--111",
}

@InProceedings{[ERS],
	author = "Z. Khasidashvili",
	title = "Expression Reduction Systems",
	booktitle = "Proceedings of I.~Vekua Institute of Applied Mathematics of Tbilisi State University",
	volume = 36,
	pages = "200--220",
	address = "Tbilisi",
	year = 1990,
}

@TechReport{[OCRS],
	author = "Z. Khasidashvili",
	title = "The {Church-Rosser} Theorem in Orthogonal Combinatory Reduction Systems",
	number = 1825,
	institution = "INRIA Rocquencourt",
	year = 1992,
}


@InProceedings{[rta],
	author = "Z. Khasidashvili",
	title = "Optimal Normalization in Orthogonal Term Rewriting Systems",
	booktitle = "$5^{th}$ International Conference on Rewriting Techniques and Applications, RTA'93, Montreal",
	publisher = SV,
	series = LNCS,
	volume = 690,
	editor = "C. Kirchner",
	pages = "243-258",
	year = 1993, 
}

@InProceedings{[caap],
	author = "Z. Khasidashvili",
	title = "On Higher Order Recursive Program Schemes",
	booktitle = "$19^{th}$ International Colloquium on Trees in Algebra and Programming, CAAP'94, Edinburgh",
	publisher = SV,
	series = LNCS,
	volume = 787,
	editor = "S. Tison",
	pages = "172-186",
	year = 1994,
}

@Article{[pun-ic],
	author = "Z. Khasidashvili and M. Ogawa and V. van Oostrom",
	title = "Perpetuality and Uniform Normalization in Orthogonal Rewrite Systems",
	journal = "Information and Computation",
	year = "To appear",
	note = "Available from http://www.brl.ntt.co.jp/people/mizuhito/papers/TRS.html",
}

@InProceedings{[KP99],
	author = "Z. Khasidashvili and A. Piperno",
	title = "Normalization of Typeable Terms by Superdevelopments",
	booktitle = "Proceedings of CSL'98",
	publisher = SV,
	series = LNCS,
	volume = 1584, 
	pages = "260--282", 
	year = 1999, 
}

@Book{[Kl.CRS],
	author = "J. W. Klop",
	title = "Combinatory Reduction Systems",
	series = "Mathematical Centre Tracts",
	volume = 127,
	publisher = "CWI, Amsterdam",
	year = 1980,
}

@InCollection{[Klo92],
	author = "J. W. Klop",
	title = "Term  Rewriting Systems",
	editpor = "S. Abramsky and D. Gabbay and T. Maibaum",
	booktitle = "Handbook  of Logic in Computer Science", 
	volume = II, 
	publisher = OUP,
	pages = "1--116",
	year = 1992, 
}

@InProceedings{[kor],
	author = "J. K. Klop and V. van Oostrom and F. van Raamsdonk",
	title = "Combinatory Reduction Systems: Introduction and Survey",
	booktitle = "To {Corrado} {B\"ohm}", 
	series = TCS,
	volume = 121,
	pages = "279--308",
	year = 1993, 
}

@Article{[le76],
	author = "J.-J. L\'evy",
	title = "An Algebraic Interpretation of the $\lambda\beta {K}$-Calculus; and an Application of a Labelled Lambda Calculus",
	journal = TCS,
	volume = 2,
	pages = "97--114",
	year = 1976, 
}

@Book{[levy],
	author = "J.-J. L\'evy",
	title = "R\'eductions Correctes et Optimales dans le Lambda-Calcul",
	publisher = "Th\`ese de l'Uni\-ver\-sit\'e de {Paris} {VII}",
	year = 1978,
}

@InCollection{[le80],
	author = "J.-J. L\'evy",
	title = "Optimal Reductions in the Lambda-Calculus",
	booktitle = "To {H. B. Curry}: Essays on Combinatory Logic, Lambda-calculus and Formalism",
	editor = "J. R. Hindley and J. P. Seldin",
	publisher = "Academic Press",
	pages = "159--192",
	year = 1980, 
}

@Article{[Lon],
	author = "G. Longo",
	title = "Set Theoretic Models of Lambda Calculus: Theories, Expansions and Isomorphisms",
	journal = "Annals of Pure and Applied Logic", 
	volume = 24,
	pages = "53--188",
	year = 1983, 
}

@InProceedings{[Mar91],
	author = "L. Maranget",
	title = "Optimal Derivations in Weak Lambda-Calculi and in Orthogonal Term Rewriting Systems",
	booktitle = "$17^{th}$ ACM Symposium on Principles of Programming Languages, POPL'91",
	publisher = ACM,
	pages = "255--269",
	year = 1991, 
}


@Book{[Mar],
	author = "L. Maranget",
	title = "La Strat\'egie Paresseuse",
	publisher = "Th\`ese de l'Universit\'e de {Paris} {VII}",
	year = 1992,
}

@Article{[MN98],
	author = "R. Mayr and T. Nipkow",
	title = "Higher-Order Rewrite Systems and Their Confluence",
	journal = TCS,
	volume = 192,
	pages = "3--29",
	year = 1998,
}

@Book{[Mel],
	author = "P.-A. Melli\`es",
	title = "Description Abstraite des Syst\`emes de R\'e\'ecriture",
	publisher = "Th\`ese de l'Uni\-versit\'e {Paris} {VII}",
	year = 1996,
}

@InProceedings{[Mel98],
	author = "P. -A. Melli\`es",
	title = "A Stability Theorem for Rewriting Theory",
	booktitle = "Proceedings of LICS'98",
	year = 1998,
}

@InProceedings{[Mid],
	author = "A. Middeldorp",
	title = "Call by Need Computations to Root-Stable Form",
	booktitle = "$24^{th}$ ACM Symposium on Principles of Programming Languages, POPL'97",
	publisher = ACM,
	pages = "94--105",
	year = 1997, 
}

@PhDThesis{[Nok.thi.],
	author = "E. {N\"ocker}",
	title = "Efficient Functional Programming: Compilation and Programming Techniques",
	school = "University of Nijmegen",
	year = 1994,
}

@PhDThesis{[Oos.th],
	author = "V. van Oostrom",
	title = "Confluence for Abstract and Higher-Order Rewriting",
	school = "Free University, Amsterdam",
	year = 1994,
}

@InProceedings{[OR94],
	author = "V. van Oostrom and F. van Raamsdonk",
	title = "Weak Orthogonality Implies Confluence: The Higher-Order Case",
	booktitle = "$3^{rd}$ International Conference on Logical Foundations of Computer Science, LFCS'94",
	publisher = SV,
	series = LNCS, 
	volume = 813,
	editor = "A. Narode and Yu. V. Matiyasevich",
	pages = "379--392",
	year = 1994,
}

@InProceedings{[Oos],
	author = "V. van Oostrom",
	title = "Higher Order Families",
	booktitle = "$7^{th}$ International Conference on Rewriting Techniques and Applications, RTA'96",
	publisher = SV,
	series = LNCS, 
	volume = 1103,
	editor = "H. Ganzinger",
	pages = "392--407",
	year = 1996, 
}

@InProceedings{[Oos97],
	author = "V. van Oostrom",
	title = "Finite Family Developments",
	booktitle = "$8^{th}$  International Conference on Rewriting Techniques and Applications, RTA'97",
	publisher = SV,
	series = LNCS, 
	volume = 1232,
	editor = "H. Common",
	pages = "308--322",
	year = 1997, 
}

@InProceedings{[Oos99],
	author = "V. van Oostrom",
	title = "Normalisation in Weakly Orthogonal Rewriting",
	booktitle = "$10^{th}$ International Conference on Rewriting Techniques and Applications, RTA'99",
	publisher = SV,
	series = LNCS, 
	volume = 1631,
	pages = "60--74",
	year = 1999, 
}

@InProceedings{[Pk],
	author = "Sh. Pkhakadze",
	title = "Some Problems of the Notation Theory (in {Russian})",
	booktitle = "Proceedings of I.~Vekua Institute of Applied Mathematics of Tbilisi State University",
	address = "Tbilisi",
	year = 1977,
}

@PhDThesis{[Raa.th],
	author = "F. van Raamsdonk",
	title = "Confluence and Normalisation for Higher-Order Rewriting",
	school = "Free University, Amsterdam",
	year = 1996,
}

@Article{[SeRa],
	author = "R. C. Sekar and I. V. Ramakrishnan",
	title = "Programming in Equational Logic: Beyond Strong Sequentiality",
	journal = "Information and Computation", 
	volume = 104,
	number = 1,
	pages = "78--109",
	year = 1993, 
}

@InProceedings{[Win89],
	author = "G. Winskel",
	title = "An Introduction to Event Structures",
	booktitle = "Linear Time, Branching Time and Partial Order in Logics and Models of Concurrency",
	publisher = SV,
	series = LNCS, 
	volume = 354,
	year = 1989, 
	pages = "364--397",
}

@Book{[Wol.th],
	author = "D. A. Wolfram",
	title = "The Clausal Theory of Types",
	series = "Cambridge Tracts in Theoretical Computer Science", 
	volume = 21,
	publisher = CUP,
	year = 1993,
}