Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
P. Aczel. A general Church-Rosser theorem. University of Manchester, July 1978.
A. Asperti and C. Laneve. Interaction systems I: The theory of optimal reductions. Mathematical Structures in Computer Science, 4:457–504, 1994.
H.P. Barendregt. The Lambda Calculus, its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, revised edition, 1984.
J.A. Bergstra and J.W. Klop. Conditional rewrite rules: Confluence and termination. Journal of Computer and System Sciences, 32:323–362, 1986.
Alonzo Church and J.B. Rosser. Some properties of conversion. Transactions of the Americal Mathematical Society, 39:472–482, 1936.
N. Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science, 17(3):279–301, 1982.
R.O. Gandy. Proofs of strong normalization. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 457–477. Academic Press, 1980.
J. Glauert and Z. Khasidashvili. Relative normalization in deterministic residual structures. In Proceedings of the 19th International Colloquium on Trees in Algebras and Programming (CAAP’ 96), volume 1059 of Lecture Notes in Computer Science, pages 180–195, April 1996.
M. Hanus and C. Prehofer. Higher-order narrowing with definitional trees. In H. Ganzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA’ 96), volume 1103 of Lecture Notes in Computer Science, pages 138–152, New Brunswick, USA, 1996.
R. Hindley. Reductions of residuals are finite. Transactions of the Americal Mathematical Society, 240:345–361, June 1978.
G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the Association for Computing Machinery, 27(4):797–821, October 1980.
G. Huet and D.C. Oppen. Equations and rewrite rules, a survey. In R.V. Book, editor, Formal Language Theory, Perspectives and Open Problems, pages 349–405. Academic Press, 1980.
J.-P. Jouannaud and A. Rubio. The higher-order recursive path ordering. In Proceedings of the 14th annual IEEE Symposium on Logic in Computer Science (LICS’ 99), Trento, Italy, 1999. To appear.
S. Kahrs. Termination proofs in an abstract setting. To appear in Mathematical Structures in Computer Science.
Z.O. Khasidashvili. Expression Reduction Systems. In Proceedings of I. Vekua Institute of Applied Mathematics, volume 36, pages 200–220, Tblisi, 1990.
J.W. Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. CWI, Amsterdam, 1980. PhD Thesis.
D.E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, 1970.
R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192:3–29, 1998.
P.-A. Melliès. Description Abstraite des Systémes de Réécriture. PhD thesis, Université de Paris VII, Paris, France, 1996.
A. Middeldorp. Call by need computations to root-stable form. In Proceedings of the 24th Symposium on Principles of Programming Languages (POPL’ 97), pages 94–105, Paris, France, January 1997. ACM Press.
D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.
T. Nipkow. Higher-order critical pairs. In Proceedings of the 6th annual IEEE Symposium on Logic in Computer Science (LICS’ 91), pages 342–349, Amsterdam, The Netherlands, July 1991.
T. Nipkow and C. Prehofer. Higher-order rewriting and equational reasoning. In W. Bibel and P. Schmitt, editors, Automated Deduction — A Basis for Applications. Volume I: Foundations, volume 8 of Applied Logic Series, pages 399–430. Kluwer, 1998.
M.J. O’Donnell. Computing in Systems Described by Equations, volume 58 of Lecture Notes in Computer Science. Springer Verlag, 1977.
V. van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhDthesis, Vrije Universiteit, Amsterdam, The Netherlands, March 1994.
V. van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159–181, 1997.
V. van Oostrom. Normalisation in weakly orthogonal rewriting. In Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA’ 99), 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Raamsdonk, F. (1999). Higher-Order Rewriting. In: Narendran, P., Rusinowitch, M. (eds) Rewriting Techniques and Applications. RTA 1999. Lecture Notes in Computer Science, vol 1631. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48685-2_17
Download citation
DOI: https://doi.org/10.1007/3-540-48685-2_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66201-3
Online ISBN: 978-3-540-48685-5
eBook Packages: Springer Book Archive