{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:54:35Z","timestamp":1725551675158},"publisher-location":"Berlin, Heidelberg","reference-count":101,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540309116"},{"type":"electronic","value":"9783540324256"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11601548_22","type":"book-chapter","created":{"date-parts":[[2005,12,10]],"date-time":"2005-12-10T00:39:45Z","timestamp":1134175185000},"page":"496-553","source":"Crossref","is-referenced-by-count":2,"title":["Expression Reduction Systems and Extensions: An Overview"],"prefix":"10.1007","author":[{"given":"John","family":"Glauert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zurab","family":"Khasidashvili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"22_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"4","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.L., L\u00e9vy, J.-J.: Explicit substitutions. Journal of Functional Programming\u00a04(1), 375\u2013416 (1991)","journal-title":"Journal of Functional Programming"},{"key":"22_CR2","unstructured":"The Alfa proof editor, http:\/\/www.cs.chalmers.se\/~hallgren\/Alfa\/"},{"key":"22_CR3","first-page":"233","volume-title":"Proceedings of the 22nd Symposium on Principles of Programming Languages","author":"Z. Ariola","year":"1995","unstructured":"Ariola, Z., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: A call-by-need lambda calculus. In: Proceedings of the 22nd Symposium on Principles of Programming Languages, pp. 233\u2013246. ACM Press, New York (1995)"},{"key":"22_CR4","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"22_CR5","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"H. Barendregt","year":"1984","unstructured":"Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol.\u00a0103. North-Holland, Amsterdam (1984) (Revised Edition)"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Barendregt, H., Bergstra, J.A., Klop, J.-W., Volken, H.: Some notes on lambda-reduction in \u201cdegrees, reductions, and representability in the lambda calculus\u201d. Technical Report\u00a022, Department of mathematics, University of Utrecht (1976)","DOI":"10.1016\/S1385-7258(76)80001-7"},{"issue":"3","key":"22_CR7","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/0890-5401(87)90001-0","volume":"75","author":"H. Barendregt","year":"1987","unstructured":"Barendregt, H., Kennaway, R., Klop, J.-W., Sleep, M.R.: Needed reduction and spine strategies for the lambda calculus. Information and Computation\u00a075(3), 191\u2013231 (1987)","journal-title":"Information and Computation"},{"issue":"5","key":"22_CR8","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1017\/S0956796800001945","volume":"6","author":"Z.E.A. Benaissa","year":"1996","unstructured":"Benaissa, Z.E.A., Briaud, D., Lescanne, P., Rouyer-Degli, J.: \u03bb\u03c5, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming\u00a06(5), 699\u2013722 (1996)","journal-title":"Journal of Functional Programming"},{"issue":"7\/8","key":"22_CR9","first-page":"403","volume":"18","author":"J.A. Bergstra","year":"1982","unstructured":"Bergstra, J.A., Klop, J.-W.: Strong normalization and perpetual reductions in the lambda calculus. Journal of Information Processing and Cybernetics\u00a018(7\/8), 403\u2013417 (1982)","journal-title":"Journal of Information Processing and Cybernetics"},{"issue":"3","key":"22_CR10","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0022-0000(86)90033-4","volume":"32","author":"J.A. Bergstra","year":"1986","unstructured":"Bergstra, J.A., Klop, J.-W.: Conditional rewrite rules: confluence and termination. Journal of Computer and System Science\u00a032(3), 323\u2013362 (1986)","journal-title":"Journal of Computer and System Science"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-61464-8_51","volume-title":"Rewriting Techniques and Applications","author":"R. Bloo","year":"1996","unstructured":"Bloo, R., Rose, K.: Combinatory reduction systems with explicit substitution that preserve strong normalisation. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol.\u00a01103, pp. 169\u2013183. Springer, Heidelberg (1996)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-36576-1_10","volume-title":"Foundations of Software Science and Computational Structures","author":"E. Bonelli","year":"2003","unstructured":"Bonelli, E.: A normalization result for higher-order calculi with explicit substitutions. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 153\u2013168. Springer, Heidelberg (2003)"},{"key":"22_CR13","unstructured":"Bonelli, E., Kesner, D., R\u00edos, A.: De Bruijn indices for metaterms. Journal of Logic and Computation (to appear)"},{"key":"22_CR14","unstructured":"Bonelli, E., Kesner, D., R\u00edos, A.: Relating higher-order and first-order rewriting. Journal of Logic and Computatio (to appear)"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/10721975_5","volume-title":"Rewriting Techniques and Applications","author":"E. Bonelli","year":"2000","unstructured":"Bonelli, E., Kesner, D., R\u00edos, A.: A de Bruijn notation for higher-order rewriting. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 62\u201379. Springer, Heidelberg (2000)"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/3-540-45127-7_6","volume-title":"Rewriting Techniques and Applications","author":"E. Bonelli","year":"2001","unstructured":"Bonelli, E., Kesner, D., R\u00edos, A.: From higher-order to first-order rewriting (extended abstract). In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, pp. 47\u201362. Springer, Heidelberg (2001)"},{"key":"22_CR17","first-page":"169","volume-title":"Algebraic methods in semantics","author":"G. Boudol","year":"1985","unstructured":"Boudol, G.: Computational semantics of term rewriting systems. In: Nivat, M., Reynolds, J. (eds.) Algebraic methods in semantics, pp. 169\u2013236. Cambridge University Press, Cambridge (1985)"},{"key":"22_CR18","volume-title":"Elements of Mathematics, Theory of Sets","author":"N. Bourbaki","year":"1968","unstructured":"Bourbaki, N.: Elements of Mathematics, Theory of Sets. Addison-Wesley, Reading (1968)"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/BFb0014047","volume-title":"Typed Lambda Calculi and Applications","author":"D. Briaud","year":"1995","unstructured":"Briaud, D.: An explicit eta rewrite rule. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902, pp. 94\u2013108. Springer, Heidelberg (1995)"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Burstall, R., MacQueen, D., Sanella, D.: Hope: An experimental applicative language. In: Proceedings of the LISP Conference, pp. 136\u2013143. Stanford University, Computer Science Department (1980)","DOI":"10.1145\/800087.802799"},{"key":"22_CR21","first-page":"98","volume-title":"14th Symposium on Logic in Computer Science","author":"S. Cerrito","year":"1999","unstructured":"Cerrito, S., Kesner, D.: Pattern matching as cut elimination. In: 14th Symposium on Logic in Computer Science, pp. 98\u2013108. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"22_CR22","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/j.tcs.2004.03.032","volume":"323","author":"S. Cerrito","year":"2004","unstructured":"Cerrito, S., Kesner, D.: Pattern matching as cut elimination. Theoretical Computer Science\u00a0323, 71\u2013127 (2004)","journal-title":"Theoretical Computer Science"},{"key":"22_CR23","unstructured":"Cirstea, H., Kirchner, C.: \u03c1-calculus, the rewriting calculus. In: 5th International Workshop on Constraints in Computational Logics (1998)"},{"key":"22_CR24","unstructured":"The Coq Proof Assistant, http:\/\/coq.inria.fr\/"},{"key":"22_CR25","series-title":"Progress in Theoretical Computer Science","volume-title":"Categorical combinators, sequential algorithms and functional programming","author":"P.-L. Curien","year":"1986","unstructured":"Curien, P.-L.: Categorical combinators, sequential algorithms and functional programming, 1st edn. Progress in Theoretical Computer Science. Birkh\u00e4user, Basel (1986)","edition":"1"},{"key":"22_CR26","unstructured":"Curien, P.-L.: Th\u00e9r\u00e8se Hardin, and Jean-Jacques L\u00e9vy. Confluence properties of weak and strong calculi of explicit substitutions. Technical Report 1617, INRIA-Rocquencourt (1992)"},{"issue":"35","key":"22_CR27","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"5","author":"N.G. Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Mathematicae\u00a05(35), 381\u2013392 (1972)","journal-title":"Indag. Mathematicae"},{"key":"22_CR28","unstructured":"de Bruijn., N.G.: A namefree lambda calculus with facilities for internal definition of expressions and segments. Technical Report 78-WSK-03, Eindhoven University of Technology (1978)"},{"key":"22_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1007\/BFb0012855","volume-title":"9th International Conference on Automated Deduction","author":"N. Dershowitz","year":"1988","unstructured":"Dershowitz, N., Okada, M., Sivakumar, G.: Canonical conditional rewrite systems. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 538\u2013549. Springer, Heidelberg (1988)"},{"key":"22_CR30","volume-title":"10th Symposium on Logic in Computer Science","author":"G. Dowek","year":"1995","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions. In: 10th Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos (1995)"},{"key":"22_CR31","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Unification via explicit substitutions: The case of higher-order patterns. Technical Report RR3591, INRIA (1998)"},{"key":"22_CR32","unstructured":"The ELAN system, http:\/\/elan.loria.fr\/ ."},{"key":"22_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/3-540-45610-4_13","volume-title":"Rewriting Techniques and Applications","author":"J. Forest","year":"2002","unstructured":"Forest, J.: A weak calculus with explicit operators for pattern matching and substitution. In: Tison, S. (ed.) RTA 2002. LNCS, vol.\u00a02378, pp. 174\u2013191. Springer, Heidelberg (2002)"},{"key":"22_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-44881-0_9","volume-title":"Rewriting Techniques and Applications","author":"J. Forest","year":"2003","unstructured":"Forest, J., Kesnerp, D.: Expression reduction systems with patterns. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 107\u2013122. Springer, Heidelberg (2003)"},{"issue":"3","key":"22_CR35","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1093\/logcom\/10.3.323","volume":"10","author":"J. Glauert","year":"2000","unstructured":"Glauert, J., Kennaway, R., Khasidashvili, Z.: Stable results and relative normalization. Journal of Logic and Computation\u00a010(3), 323\u2013348 (2000); Special Issue: Type Theory and Term Rewriting","journal-title":"Journal of Logic and Computation"},{"key":"22_CR36","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"2nd International Workshop on Reduction Strategies in Rewriting and Programming","author":"J. Glauert","year":"2002","unstructured":"Glauert, J., Khasidashvili, Z.: An abstract B\u00f6hm-normalization. In: 2nd International Workshop on Reduction Strategies in Rewriting and Programming. Electronic Notes in Theoretical Computer Science, vol.\u00a070(6). Elsevier Science, Amsterdam (2002)"},{"key":"22_CR37","unstructured":"Gramlich, B.: Termination and confluence properties of structured rewrite systems. PhD thesis, Universit\u00e4t Kaiserslautern, Germany (1996)"},{"key":"22_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1007\/3-540-61464-8_48","volume-title":"Rewriting Techniques and Applications","author":"M. Hanus","year":"1996","unstructured":"Hanus, M., Prehofer, C.: Higher-order narrowing with definitional trees. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol.\u00a01103, pp. 138\u2013152. Springer, Heidelberg (1996)"},{"key":"22_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/BFb0013834","volume-title":"Algebraic and Logic Programming","author":"T. Hardin","year":"1992","unstructured":"Hardin, T.: \u03b7-reduction for explicit substitutions. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol.\u00a0632, pp. 306\u2013321. Springer, Heidelberg (1992)"},{"key":"22_CR40","unstructured":"Hardin, T., L\u00e9vy, J.-J.: A confluent calculus of substitutions. In: France-Japan Artificial Intelligence and Computer Science Symposium, Izu, Japan (1989)"},{"key":"22_CR41","first-page":"25","volume-title":"Proceedings of the International Conference on Functional Programming","author":"T. Hardin","year":"1996","unstructured":"Hardin, T., Maranget, L., Pagano, B.: Functional back-ends within the lambda-sigma calculus. In: Proceedings of the International Conference on Functional Programming, pp. 25\u201333. ACM Press, New York (1996)"},{"key":"22_CR42","doi-asserted-by":"crossref","unstructured":"Hudak, P., Peyton-Jones, S., Wadler, P.: Report on the programming language Haskell, a non-strict, purely functional language (version 1.2). Sigplan Notices (1992)","DOI":"10.1145\/130697.130699"},{"key":"22_CR43","first-page":"394","volume-title":"Computational Logic, Essays in Honor of Alan Robinson","author":"G. Huet","year":"1991","unstructured":"Huet, G., L\u00e9vy, J.-J.: Computations in orthogonal rewriting systems. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic, Essays in Honor of Alan Robinson, pp. 394\u2013443. MIT Press, Cambridge (1991)"},{"key":"22_CR44","unstructured":"The Isabelle theorem prover, http:\/\/isabelle.in.tum.de\/"},{"issue":"6","key":"22_CR45","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1145\/1034774.1034775","volume":"26","author":"C. Barry Jay","year":"2004","unstructured":"Barry Jay, C.: The pattern calculus. ACM Transactions on Programming Languages and Systems\u00a026(6), 911\u2013937 (2004)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"22_CR46","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1109\/LICS.1991.151659","volume-title":"6th Symposium on Logic in Computer Science","author":"J.-P. Jouannaud","year":"1991","unstructured":"Jouannaud, J.-P., Okada, M.: A computation model for executable higher-order algebraic specification languages. In: 6th Symposium on Logic in Computer Science, pp. 350\u2013361. IEEE Computer Society Press, Los Alamitos (1991)"},{"key":"22_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BFb0026813","volume-title":"Programming Languages: Implementations, Logics and Programs","author":"F. Kamareddine","year":"1995","unstructured":"Kamareddine, F., R\u00edos, A.: A \u03bb-calculus \u00e0 la de Bruijn with explicit substitutions. In: Swierstra, S.D. (ed.) PLILP 1995. LNCS, vol.\u00a0982, pp. 45\u201362. Springer, Heidelberg (1995)"},{"key":"22_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/3-540-61464-8_52","volume-title":"Rewriting Techniques and Applications","author":"D. Kesner","year":"1996","unstructured":"Kesner, D.: Confluence properties of extensional and non-extensional \u03bb-calculi with explicit substitutions. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol.\u00a01103, pp. 184\u2013199. Springer, Heidelberg (1996)"},{"issue":"1-2","key":"22_CR49","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S0304-3975(98)00166-2","volume":"238","author":"D. Kesner","year":"2000","unstructured":"Kesner, D.: Confluence of extensional and non-extensional lambda-calculi with explicit substitutions. Theoretical Computer Science\u00a0238(1-2), 183\u2013220 (2000)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"22_CR50","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1006\/inco.1996.0004","volume":"124","author":"D. Kesner","year":"1996","unstructured":"Kesner, D., Puel, L., Tannen, V.: A Typed Pattern Calculus. Information and Computation\u00a0124(1), 32\u201361 (1996)","journal-title":"Information and Computation"},{"key":"22_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/3-540-52335-9_51","volume-title":"COLOG-88","author":"Z. Khasidashvili","year":"1990","unstructured":"Khasidashvili, Z.: \u03b2-reductions and \u03b2-developments of \u03bb-terms with the least number of steps. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol.\u00a0417, pp. 105\u2013111. Springer, Heidelberg (1990)"},{"key":"22_CR52","unstructured":"Khasidashvili, Z.: Expression reduction systems. Technical Report 36: 200-220, I. Vekua Institute of Applied Mathematics of Tbilisi State University (1990)"},{"key":"22_CR53","unstructured":"Khasidashvili, Z.: The church-rosser theorem in orthogonal combinatory reduction systems. Technical Report 1825, INRIA-Rocquencourt (1992)"},{"key":"22_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/3-540-58140-5_20","volume-title":"Logical Foundations of Computer Science","author":"Z. Khasidashvili","year":"1994","unstructured":"Khasidashvili, Z.: The longest perpetual reductions in orthogonal expression reduction systems. In: Matiyasevich, Y.V., Nerode, A. (eds.) LFCS 1994. LNCS, vol.\u00a0813, pp. 191\u2013203. Springer, Heidelberg (1994)"},{"key":"22_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/BFb0017481","volume-title":"Trees in Algebra and Programming - CAAP \u201994","author":"Z. Khasidashvili","year":"1994","unstructured":"Khasidashvili, Z.: On higher order recursive program schemes. In: Tison, S. (ed.) CAAP 1994. LNCS, vol.\u00a0787, pp. 172\u2013186. Springer, Heidelberg (1994)"},{"key":"22_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/3-540-57785-8_139","volume-title":"STACS 94","author":"Z. Khasidashvili","year":"1994","unstructured":"Khasidashvili, Z.: Perpetuality and strong normalization in orthogonal term rewriting systems. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds.) STACS 1994. LNCS, vol.\u00a0775, pp. 163\u2013174. Springer, Heidelberg (1994)"},{"issue":"1\/2","key":"22_CR57","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1016\/S0304-3975(00)00372-8","volume":"266","author":"Z. Khasidashvili","year":"2001","unstructured":"Khasidashvili, Z.: On the longest perpetual reductions in orthogonal expression reduction systems. Theoretical Computer Science\u00a0266(1\/2), 737\u2013772 (2001)","journal-title":"Theoretical Computer Science"},{"key":"22_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/3-540-44881-0_33","volume-title":"Rewriting Techniques and Applications","author":"Z. Khasidashvili","year":"2003","unstructured":"Khasidashvili, Z.: Optimal normalization in orthogonal term rewriting systems. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 243\u2013258. Springer, Heidelberg (2003)"},{"issue":"1","key":"22_CR59","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0304-3975(01)00235-3","volume":"286","author":"Z. Khasidashvili","year":"2002","unstructured":"Khasidashvili, Z., Glauert, J.: Relating conflict-free stable transition and event models via redex families. Theoretical Computer Science\u00a0286(1), 65\u201395 (2002)","journal-title":"Theoretical Computer Science"},{"key":"22_CR60","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"3rd International Workshop on Reduction Strategies in Rewriting and Programming","author":"Z. Khasidashvili","year":"2003","unstructured":"Khasidashvili, Z., Glauert, J.: An abstract concept of optimal implementation. In: 3rd International Workshop on Reduction Strategies in Rewriting and Programming. Electronic Notes in Theoretical Computer Science, vol.\u00a084(4). Elsevier Science, Amsterdam (2003)"},{"key":"22_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/3-540-44881-0_33","volume-title":"Rewriting Techniques and Applications","author":"Z. Khasidashvili","year":"2003","unstructured":"Khasidashvili, Z., Glauert, J.: Stable computational semantics of conflict-free rewrite systems (partial orders with erasure). In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 467\u2013482. Springer, Heidelberg (2003)"},{"key":"22_CR62","doi-asserted-by":"crossref","unstructured":"Khasidashvili, Z., Glauert, J.: The geometry of conflict-free reduction spaces. Theoretical Computer Science (2005) (to appear)","DOI":"10.1016\/j.tcs.2004.07.037"},{"issue":"1","key":"22_CR63","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1006\/inco.2000.2888","volume":"164","author":"Z. Khasidashvili","year":"2001","unstructured":"Khasidashvili, Z., Ogawa, M., van Oostrom, V.: Perpetuality and uniform normalization in orthogonal rewrite systems. Information and Computation\u00a0164(1), 118\u2013151 (2001)","journal-title":"Information and Computation"},{"key":"22_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/BFb0027014","volume-title":"Algebraic and Logic Programming","author":"Z. Khasidashvili","year":"1997","unstructured":"Khasidashvili, Z., Piperno, A.: Perpetuality and uniform normalization. In: Hanus, M., Heering, J., Meinke, K. (eds.) ALP 1997 and HOA 1997. LNCS, vol.\u00a01298, pp. 240\u2013255. Springer, Heidelberg (1997)"},{"key":"22_CR65","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Workshop on Graph Rewriting and Computation","author":"Z. Khasidashvili","year":"1995","unstructured":"Khasidashvili, Z., van Oostrom, V.: Context-sensitive conditional expression reduction systems. In: Workshop on Graph Rewriting and Computation. Electronic Notes in Theoretical Computer Science, vol.\u00a02. Elsevier Science, Amsterdam (1995)"},{"key":"22_CR66","doi-asserted-by":"crossref","unstructured":"Khasidashvili, Z., van Oostrom, V.: Context-sensitive conditional rewrite systems. Technical Report SYS\u2013C95\u201306, University of East Anglia (1995)","DOI":"10.1016\/S1571-0661(05)80193-8"},{"key":"22_CR67","unstructured":"Klop, J.-W.: Combinatory Reduction Systems. PhD thesis, Mathematical Centre Tracts 127, CWI, Amsterdam (1980)"},{"key":"22_CR68","series-title":"Handbook of Logic in Computer Science","first-page":"1","volume-title":"Term Rewriting Systems","author":"J.-W. Klop","year":"1992","unstructured":"Klop, J.-W.: Term Rewriting Systems. Handbook of Logic in Computer Science, vol.\u00a02, pp. 1\u2013116. Oxford University Press, Oxford (1992)"},{"issue":"1\/2","key":"22_CR69","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J.-W. Klop","year":"1993","unstructured":"Klop, J.-W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theoretical Computer Science\u00a0121(1\/2), 279\u2013308 (1993)","journal-title":"Theoretical Computer Science"},{"key":"22_CR70","unstructured":"L\u00e9vy, J.-J.: R\u00e9ductions correctes et optimales dans le lambda-calcul. PhD thesis, Universit\u00e9 Paris VII, France (1978)"},{"key":"22_CR71","unstructured":"L\u00e9vy, J.-J.: Optimal reductions in the lambda-calculus. In: Hindley, J.R., Seldin, J.P., Curry, T.H.B. (eds.), pp. 159\u2013192. Academic Press, London (1980)"},{"key":"22_CR72","first-page":"255","volume-title":"Proceedings of the 18th Symposium on Principles of Programming Languages","author":"L. Maranget","year":"1991","unstructured":"Maranget, L.: Optimal derivations in weak lambda-calculi and in orthogonal term rewriting systems. In: Proceedings of the 18th Symposium on Principles of Programming Languages, pp. 255\u2013269. ACM Press, New York (1991)"},{"key":"22_CR73","unstructured":"The MAUDE System, http:\/\/maude.cs.uiuc.edu\/"},{"key":"22_CR74","unstructured":"Melli\u00e8s, P.-A.: Description Abstraite des Syst\u00e8mes de R\u00e9\u00e9criture. PhD thesis, Universit\u00e9 Paris VII (1996)"},{"issue":"3","key":"22_CR75","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1093\/logcom\/10.3.461","volume":"10","author":"P.-A. Melli\u00e8s","year":"2000","unstructured":"Melli\u00e8s, P.-A.: Axiomatic rewriting theory II: the lambda-sigma calculus enjoys finite normalisation cones. Journal of Logic and Computation\u00a010(3), 461\u2013487 (2000)","journal-title":"Journal of Logic and Computation"},{"key":"22_CR76","first-page":"94","volume-title":"Proceedings of the 24th Symposium on Principles of Programming Languages","author":"A. Middeldorp","year":"1997","unstructured":"Middeldorp, A.: Call by need computations to root-stable form. In: Proceedings of the 24th Symposium on Principles of Programming Languages, pp. 94\u2013105. ACM Press, New York (1997)"},{"issue":"2","key":"22_CR77","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1017\/S0960129500001407","volume":"2","author":"R. Milner","year":"2005","unstructured":"Milner, R.: Functions as processes. Mathematical Structures in Computer Science\u00a02(2), 119\u2013141 (2005)","journal-title":"Mathematical Structures in Computer Science"},{"key":"22_CR78","volume-title":"The definition of Standard ML","author":"R. Milner","year":"1990","unstructured":"Milner, R., Tofte, M., Harper, R.: The definition of Standard ML. MIT Press, Cambridge (1990)"},{"key":"22_CR79","series-title":"Lecture Notes in Computer Science","first-page":"224","volume-title":"Join International Conference on Algebraic and Logic Programming and International Workshop on Higher-Order Algebra","author":"C. Mu\u00f1oz","year":"1997","unstructured":"Mu\u00f1oz, C.: A left-linear variant of \u03bb\u03c3. In: Join International Conference on Algebraic and Logic Programming and International Workshop on Higher-Order Algebra. LNCS, vol.\u00a01298, pp. 224\u2013239. Springer, Heidelberg (1997)"},{"key":"22_CR80","unstructured":"Nederpelt, R.: Strong normalization for a typed lambda-calculus with lambda structured types. PhD thesis, Technische Hogeschool Eindhoven, Netherlands (1973)"},{"key":"22_CR81","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1109\/LICS.1991.151658","volume-title":"6th Symposium on Logic in Computer Science","author":"T. Nipkow","year":"1991","unstructured":"Nipkow, T.: Higher-order critical pairs. In: 6th Symposium on Logic in Computer Science, pp. 342\u2013349. IEEE Computer Society Press, Los Alamitos (1991)"},{"key":"22_CR82","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/BFb0037114","volume-title":"Typed Lambda Calculi and Applications","author":"T. Nipkow","year":"1993","unstructured":"Nipkow, T.: Orthogonal higher-order rewrite systems are confluent. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 306\u2013317. Springer, Heidelberg (1993)"},{"key":"22_CR83","unstructured":"N\u00f6cker, E.: Efficient Functional Programming: Compilation and Programming Techniques. PhD thesis, University of Nijmegen, Netherlands (1994)"},{"key":"22_CR84","unstructured":"The Objective Caml language, http:\/\/caml.inria.fr\/"},{"key":"22_CR85","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-08531-9","volume-title":"Computing in Systems Described by Equations","author":"M.J. O\u2019Donnell","year":"1977","unstructured":"O\u2019Donnell, M.J.: Computing in Systems Described by Equations. LNCS, vol.\u00a058. Springer, Heidelberg (1977)"},{"key":"22_CR86","unstructured":"Pkhakadze, S.: Some problems of the notation theory. I. Vekua Institute of Applied Mathematics of Tbilisi State University (1977) (in Russian)"},{"issue":"2","key":"22_CR87","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1023\/A:1022128817224","volume":"6","author":"S. Pkhakadze","year":"1999","unstructured":"Pkhakadze, S.: An n. bourbaki-type general theory and the properties of contracting symbols and corresponding contracted forms. Georgian Mathematical Journal\u00a06(2), 179\u2013190 (1999)","journal-title":"Georgian Mathematical Journal"},{"key":"22_CR88","series-title":"Lecture Notes in Computer Science","first-page":"405","volume-title":"Rewriting Techniques and Applications","author":"D. Plaisted","year":"2003","unstructured":"Plaisted, D.: Polynomial time termination and constraint satisfaction tests. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 405\u2013420. Springer, Heidelberg (2003)"},{"key":"22_CR89","unstructured":"The PVS system, http:\/\/pvs.csl.sri.com\/"},{"key":"22_CR90","unstructured":"R\u00edos, A.: Contribution \u00e0 l\u2019\u00e9tude des \u03bb-calculs avec substitutions explicites. Th\u00e8se de doctorat, Universit\u00e9 de Paris VII (1993)"},{"key":"22_CR91","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/3-540-56393-8_3","volume-title":"Conditional Term Rewriting Systems","author":"K. Rose","year":"1993","unstructured":"Rose, K.: Explicit cyclic substitutions. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol.\u00a0656, pp. 36\u201350. Springer, Heidelberg (1993)"},{"key":"22_CR92","unstructured":"S\u00f8rensen, M.H.: Normalization in \u03bb-calculus and type theory. PhD thesis, University of Copenhagen, Denmark (1997)"},{"key":"22_CR93","first-page":"353","volume-title":"1st Tbilisi Symposium on Logic, Language and Computation, Selected papers","author":"M.H. S\u00f8rensen","year":"1998","unstructured":"S\u00f8rensen, M.H.: Properties of infinite reduction paths in untyped \u03bb-calculus. In: 1st Tbilisi Symposium on Logic, Language and Computation, Selected papers, pp. 353\u2013367. SiLLI Publications, CSLI, Stanford (1998)"},{"key":"22_CR94","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Term Rewriting Systems","author":"Terese","year":"2003","unstructured":"Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol.\u00a055. Cambridge University Press, Cambridge (2003)"},{"key":"22_CR95","series-title":"Lecture Notes in Computer Science","first-page":"128","volume-title":"Conditional Term Rewriting Systems","author":"Y. Toyama","year":"1988","unstructured":"Toyama, Y.: Confluent term rewriting systems with membership conditions. In: Kaplan, S., Jouannaud, J.-P. (eds.) CTRS 1987. LNCS, vol.\u00a0308, pp. 128\u2013141. Springer, Heidelberg (1988)"},{"key":"22_CR96","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Functional Programming Languages and Computer Architecture","author":"D. Turner","year":"1985","unstructured":"Turner, D.: Miranda: A non-strict functional language with polymorphic types. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol.\u00a0201, pp. 1\u201316. Springer, Heidelberg (1985)"},{"key":"22_CR97","unstructured":"van Oostrom, V.: Confluence for Abstract and Higher-order Rewriting. PhD thesis, Vrije University, Amsterdam, Netherlands (1994)"},{"key":"22_CR98","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/3-540-58140-5_35","volume-title":"Logical Foundations of Computer Science","author":"V. Oostrom van","year":"1994","unstructured":"van Oostrom, V., van Raamsdonk, F.: Weak orthogonality implies confluence: the higher-order case. In: Matiyasevich, Y.V., Nerode, A. (eds.) LFCS 1994. LNCS, vol.\u00a0813, pp. 379\u2013392. Springer, Heidelberg (1994)"},{"key":"22_CR99","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/3-540-56868-9_14","volume-title":"Rewriting Techniques and Applications","author":"F. Raamsdonk van","year":"1993","unstructured":"van Raamsdonk, F.: Confluence and superdevelopments. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol.\u00a0690, pp. 168\u2013182. Springer, Heidelberg (1993)"},{"issue":"2","key":"22_CR100","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1006\/inco.1998.2750","volume":"149","author":"F. Raamsdonk van","year":"1999","unstructured":"van Raamsdonk, F., Severi, P., S\u00f8rensen, M.H., Xi, H.: Perpetual reductions in \u03bb-calculus. Information and Computation\u00a0149(2), 173\u2013229 (1999)","journal-title":"Information and Computation"},{"key":"22_CR101","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569906","volume-title":"The Causal Theory of Types","author":"D. Wolfram","year":"1993","unstructured":"Wolfram, D.: The Causal Theory of Types. Cambridge Tracts in Theoretical Computer Science, vol.\u00a021. Cambridge University Press, Cambridge (1993)"}],"container-title":["Lecture Notes in Computer Science","Processes, Terms and Cycles: Steps on the Road to Infinity"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11601548_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T17:13:12Z","timestamp":1683306792000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11601548_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540309116","9783540324256"],"references-count":101,"URL":"https:\/\/doi.org\/10.1007\/11601548_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}