\newcommand{\bibnoop}[1]{}\newcommand{\bibsingleletter}[1]{#1}
\begin{thebibliography}{10}

\bibitem{[Acz]}
P.~Aczel.
\newblock A general {Church}-{Rosser} theorem.
\newblock Technical report, University of Manchester, 1978.

\bibitem{[Ant]}
S.~Antoy, R.~Echahed, and M.~Hanus.
\newblock A needed narrowing strategy.
\newblock In {\em $21^{st}$ ACM Symposium on Principles of Programming
  Languages, POPL'94}, pages 268--279. ACM, 1994.

\bibitem{[AnMi]}
S.~Antoy and A.~Middeldorp.
\newblock A sequential reduction strategy.
\newblock {\em Theoretical Computer Science}, 165(1):75--95, 1996.

\bibitem{[AL]}
A.~Asperti and C.~Laneve.
\newblock Interaction {Systems} {I}: The theory of optimal reductions.
\newblock {\em Mathematical Structures in Computer Science}, 11:1--48, 1993.

\bibitem{[Bar]}
H.~P. Barendregt.
\newblock {\em The Lambda Calculus, its Syntax and Semantics}.
\newblock North-Holland, 1984.

\bibitem{[BBKV]}
H.~P. Barendregt, J.~Bergstra, J.~W. Klop, and H.~Volken.
\newblock Degrees, reductions and representability in the $\lambda$-calculus.
\newblock Technical Report~22, University of Utrecht, 1976.

\bibitem{[B.K.K.S.]}
H.~P. Barendregt, J.~R. Kennaway, J.~W. Klop, and M.~R. Sleep.
\newblock Needed reduction and spine strategies for the lambda calculus.
\newblock {\em Information and Computation}, 75(3):191--231, 1987.

\bibitem{[B.L.]}
G.~Berry and J.-J. L\'evy.
\newblock Minimal and optimal computations of recursive programs.
\newblock {\em Journal of the ACM}, 26:148--175, 1979.

\bibitem{[Bou]}
G.~Boudol.
\newblock Computational semantics of term rewriting systems.
\newblock In M.~Nivat and J.~C. Reynolds, editors, {\em Algebraic Methods in
  Semantics}, pages 169--236. Cambridge University Press, 1985.

\bibitem{[C.F.]}
H.~B. Curry and R.~Feys.
\newblock {\em Combinatory Logic}, volume~1.
\newblock North-Holland, 1958.

\bibitem{[Gar]}
P.~Gardner.
\newblock Discovering needed reductions using type theory.
\newblock In M.~Hagiya and J.~C. Mitchell, editors, {\em $2^{nd}$ International
  Symposium on Theoretical Aspects of Computer Software, TACS'94}, volume 789
  of {\em LNCS}, pages 555--574. Springer-Verlag, 1994.

\bibitem{[morn]}
J.~R.~W. Glauert and Z.~Khasidashvili.
\newblock Minimal and optimal relative normalization in expression reduction
  systems.
\newblock Technical Report SYS-C94-06, UEA, Norwich, UK, 1994.

\bibitem{[ctrs]}
J.~R.~W. Glauert and Z.~Khasidashvili.
\newblock On relative normalization in orthogonal expression reduction systems.
\newblock In N.~Dershowitz and N.~Lindenstrauss, editors, {\em $4^{th}$
  International Workshop on Conditional (and Typed) Term Rewriting Systems,
  CTRS'94}, volume 968 of {\em LNCS}, pages 144--165. Springer-Verlag, 1994.

\bibitem{[fsttcs]}
J.~R.~W. Glauert and Z.~Khasidashvili.
\newblock Minimal relative normalization in orthogonal expression reduction
  systems.
\newblock In V.~Chandru, editor, {\em $16^{th}$ International Conference on
  Foundations of Software Technology and Theoretical Computer Science,
  FST\&TCS'96}, volume 1180 of {\em LNCS}, pages 238--249, 1996.

\bibitem{[rndrs]}
J.~R.~W. Glauert and Z.~Khasidashvili.
\newblock Relative normalization in deterministic residual structures.
\newblock In H.~Kirchner, editor, {\em $19^{th}$ International Colloquium on
  Trees in Algebra and Programming, CAAP'96}, volume 1059 of {\em LNCS}, pages
  180--195. Springer-Verlag, 1996.

\bibitem{[GLM]}
G.~Gonthier, J.-J. L\'evy, and P.-A. Melli\`es.
\newblock An abstract standardisation theorem.
\newblock In {\em $7^{th}$ Annual IEEE Symposium on Logic in Computer Science,
  LICS'92}, pages 72--81. The IEEE Computer Society Press, 1992.

\bibitem{[HP96]}
M.~Hanus and C.~Prehofer.
\newblock Higher-order narrowing with definitional trees.
\newblock In H.~Ganzinger, editor, {\em $7^{th}$ International Conference on
  Rewriting Techniques and Applications, RTA'96}, volume 1103 of {\em LNCS},
  pages 138--152. Springer-Verlag, 1996.

\bibitem{[H.L.]}
G.~Huet and J.-J. L\'evy.
\newblock Computations in orthogonal rewriting systems.
\newblock In J.-L. Lassez and G.~Plotkin, editors, {\em Computational Logic,
  Essays in Honor of Alan Robinson}. MIT Press, 1991.

\bibitem{[Kenn]}
J.~R. Kennaway.
\newblock Sequential evaluation strategies for parallel-or and related
  reduction systems.
\newblock {\em Annals of Pure and Applied Logic}, 43:31--56, 1989.

\bibitem{[K-tra]}
J.~R. Kennaway, J.~W. Klop, M.~R. Sleep, and F.-J. de~Vries.
\newblock Transfinite reductions in orthogonal term rewriting.
\newblock {\em Information and Computation}, 119(1):18--38, 1995.

\bibitem{[K.S.]}
J.~R. Kennaway and M.~R. Sleep.
\newblock Neededness is hypernormalizing in regular combinatory reduction
  systems.
\newblock Technical report, UEA, Norwich, UK, 1989.

\bibitem{[colog]}
Z.~Khasidashvili.
\newblock $\beta$-reductions and $\beta$-developments of $\lambda$-terms with
  the least number of steps.
\newblock In P.~Martin-{L\"of} and G.~Mints, editors, {\em International
  Conference on Computer Logic, COLOG'88}, volume 417 of {\em LNCS}, pages
  105--111. Springer-Verlag, 1990.

\bibitem{[ERS]}
Z.~Khasidashvili.
\newblock Expression reduction systems.
\newblock In {\em Proceedings of I.~Vekua Institute of Applied Mathematics of
  Tbilisi State University}, volume~36, pages 200--220, Tbilisi, 1990.

\bibitem{[OCRS]}
Z.~Khasidashvili.
\newblock The {Church-Rosser} theorem in orthogonal combinatory reduction
  systems.
\newblock Technical Report 1825, INRIA Rocquencourt, 1992.

\bibitem{[rta]}
Z.~Khasidashvili.
\newblock Optimal normalization in orthogonal term rewriting systems.
\newblock In C.~Kirchner, editor, {\em $5^{th}$ International Conference on
  Rewriting Techniques and Applications, RTA'93, Montreal}, volume 690 of {\em
  LNCS}, pages 243--258. Springer-Verlag, 1993.

\bibitem{[caap]}
Z.~Khasidashvili.
\newblock On higher order recursive program schemes.
\newblock In S.~Tison, editor, {\em $19^{th}$ International Colloquium on Trees
  in Algebra and Programming, CAAP'94, Edinburgh}, volume 787 of {\em LNCS},
  pages 172--186. Springer-Verlag, 1994.

\bibitem{[pun-ic]}
Z.~Khasidashvili, M.~Ogawa, and V.~van Oostrom.
\newblock Perpetuality and uniform normalization in orthogonal rewrite systems.
\newblock {\em Information and Computation}, To appear.
\newblock Available from
  http://www.brl.ntt.co.jp/people/mizuhito/papers/TRS.html.

\bibitem{[KP99]}
Z.~Khasidashvili and A.~Piperno.
\newblock Normalization of typeable terms by superdevelopments.
\newblock In {\em Proceedings of CSL'98}, volume 1584 of {\em LNCS}, pages
  260--282. Springer-Verlag, 1999.

\bibitem{[Kl.CRS]}
J.~W. Klop.
\newblock {\em Combinatory Reduction Systems}, volume 127 of {\em Mathematical
  Centre Tracts}.
\newblock CWI, Amsterdam, 1980.

\bibitem{[le76]}
J.-J. L\'evy.
\newblock An algebraic interpretation of the $\lambda\beta {K}$-calculus; and
  an application of a labelled lambda calculus.
\newblock {\em Theoretical Computer Science}, 2:97--114, 1976.

\bibitem{[levy]}
J.-J. L\'evy.
\newblock {\em R\'eductions Correctes et Optimales dans le Lambda-Calcul}.
\newblock Th\`ese de l'Uni\-ver\-sit\'e de {Paris} {VII}, 1978.

\bibitem{[le80]}
J.-J. L\'evy.
\newblock Optimal reductions in the lambda-calculus.
\newblock In J.~R. Hindley and J.~P. Seldin, editors, {\em To {H. B. Curry}:
  Essays on Combinatory Logic, Lambda-calculus and Formalism}, pages 159--192.
  Academic Press, 1980.

\bibitem{[Lon]}
G.~Longo.
\newblock Set theoretic models of lambda calculus: Theories, expansions and
  isomorphisms.
\newblock {\em Annals of Pure and Applied Logic}, 24:53--188, 1983.

\bibitem{[Mar91]}
L.~Maranget.
\newblock Optimal derivations in weak lambda-calculi and in orthogonal term
  rewriting systems.
\newblock In {\em $17^{th}$ ACM Symposium on Principles of Programming
  Languages, POPL'91}, pages 255--269. ACM, 1991.

\bibitem{[Mar]}
L.~Maranget.
\newblock {\em La Strat\'egie Paresseuse}.
\newblock Th\`ese de l'Universit\'e de {Paris} {VII}, 1992.

\bibitem{[MN98]}
R.~Mayr and T.~Nipkow.
\newblock Higher-order rewrite systems and their confluence.
\newblock {\em Theoretical Computer Science}, 192:3--29, 1998.

\bibitem{[Mel]}
P.-A. Melli\`es.
\newblock {\em Description Abstraite des Syst\`emes de R\'e\'ecriture}.
\newblock Th\`ese de l'Uni\-versit\'e {Paris} {VII}, 1996.

\bibitem{[Mel98]}
P.~A. Melli\`es.
\newblock A stability theorem for rewriting theory.
\newblock In {\em Proceedings of LICS'98}, 1998.

\bibitem{[Mid]}
A.~Middeldorp.
\newblock Call by need computations to root-stable form.
\newblock In {\em $24^{th}$ ACM Symposium on Principles of Programming
  Languages, POPL'97}, pages 94--105. ACM, 1997.

\bibitem{[Nok.thi.]}
E.~{N\"ocker}.
\newblock {\em Efficient Functional Programming: Compilation and Programming
  Techniques}.
\newblock PhD thesis, University of Nijmegen, 1994.

\bibitem{[Pk]}
Sh. Pkhakadze.
\newblock Some problems of the notation theory (in {Russian}).
\newblock In {\em Proceedings of I.~Vekua Institute of Applied Mathematics of
  Tbilisi State University}, Tbilisi, 1977.

\bibitem{[SeRa]}
R.~C. Sekar and I.~V. Ramakrishnan.
\newblock Programming in equational logic: Beyond strong sequentiality.
\newblock {\em Information and Computation}, 104(1):78--109, 1993.

\bibitem{[Oos.th]}
V.~van Oostrom.
\newblock {\em Confluence for Abstract and Higher-Order Rewriting}.
\newblock PhD thesis, Free University, Amsterdam, 1994.

\bibitem{[Oos]}
V.~van Oostrom.
\newblock Higher order families.
\newblock In H.~Ganzinger, editor, {\em $7^{th}$ International Conference on
  Rewriting Techniques and Applications, RTA'96}, volume 1103 of {\em LNCS},
  pages 392--407. Springer-Verlag, 1996.

\bibitem{[Oos97]}
V.~van Oostrom.
\newblock Finite family developments.
\newblock In H.~Common, editor, {\em $8^{th}$ International Conference on
  Rewriting Techniques and Applications, RTA'97}, volume 1232 of {\em LNCS},
  pages 308--322. Springer-Verlag, 1997.

\bibitem{[Oos99]}
V.~van Oostrom.
\newblock Normalisation in weakly orthogonal rewriting.
\newblock In {\em $10^{th}$ International Conference on Rewriting Techniques
  and Applications, RTA'99}, volume 1631 of {\em LNCS}, pages 60--74.
  Springer-Verlag, 1999.

\bibitem{[OR94]}
V.~van Oostrom and F.~van Raamsdonk.
\newblock Weak orthogonality implies confluence: The higher-order case.
\newblock In A.~Narode and Yu.~V. Matiyasevich, editors, {\em $3^{rd}$
  International Conference on Logical Foundations of Computer Science,
  LFCS'94}, volume 813 of {\em LNCS}, pages 379--392. Springer-Verlag, 1994.

\bibitem{[Raa.th]}
F.~van Raamsdonk.
\newblock {\em Confluence and Normalisation for Higher-Order Rewriting}.
\newblock PhD thesis, Free University, Amsterdam, 1996.

\bibitem{[Win89]}
G.~Winskel.
\newblock An introduction to event structures.
\newblock In {\em Linear Time, Branching Time and Partial Order in Logics and
  Models of Concurrency}, volume 354 of {\em LNCS}, pages 364--397.
  Springer-Verlag, 1989.

\bibitem{[Wol.th]}
D.~A. Wolfram.
\newblock {\em The Clausal Theory of Types}, volume~21 of {\em Cambridge Tracts
  in Theoretical Computer Science}.
\newblock Cambridge University Press, 1993.

\end{thebibliography}