{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:19:07Z","timestamp":1742617147580,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540620341"},{"type":"electronic","value":"9783540496311"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-62034-6_53","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:31:44Z","timestamp":1330295504000},"page":"238-249","source":"Crossref","is-referenced-by-count":1,"title":["Minimal relative normalization in orthogonal expression reduction systems"],"prefix":"10.1007","author":[{"given":"John","family":"Glauert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zurab","family":"Khasidashvili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1006\/inco.1993.1044","volume":"105","author":"S. Abramsky","year":"1993","unstructured":"Abramsky S., Ong C.-H. L. Full abstraction in the lazy lambda calculus. Inf.& Comp., 105:159\u2013267, 1993.","journal-title":"Inf.& Comp."},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Antoy S., Echahed R., Hanus M. A needed narrowing strategy. In: Proc. of POPL'94, Portland, Oregon, 1994.","DOI":"10.1145\/174675.177899"},{"key":"21_CR3","first-page":"168","volume":"850","author":"S. Antoy","year":"1994","unstructured":"Antoy S. and Middeldorp A. A Sequential Reduction Strategy. In Proc. of ALP'94, Springer LNCS, vol. 850, p. 168\u2013185, 1994.","journal-title":"Springer LNCS"},{"key":"21_CR4","unstructured":"Asperti A., Laneve C. Interaction Systems I: the theory of optimal reductions. MSCS, 11:1\u201348, Cambridge University Press, 1993."},{"key":"21_CR5","unstructured":"Barendregt H. P. The Lambda Calculus, its Syntax and Semantics. North-Holland, 1984."},{"issue":"3","key":"21_CR6","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/0890-5401(87)90001-0","volume":"75","author":"H. P. Barendregt","year":"1987","unstructured":"Barendregt H. P., Kennaway J. R., Klop J. W., Sleep M. R. Needed Reduction and spine strategies for the lambda calculus. Inf.& Comp., 75(3):191\u2013231, 1987.","journal-title":"Inf.& Comp."},{"key":"21_CR7","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1145\/322108.322122","volume":"26","author":"G. Berry","year":"1979","unstructured":"Berry G., L\u00e9vy J.-J. Minimal and optimal computations of recursive programs. JACM 26, 1979, p. 148\u2013175.","journal-title":"JACM"},{"key":"21_CR8","unstructured":"Boudol G. Computational semantics of term rewriting systems. In: Algebraic methods in semantics. Nivat M., Reynolds J.C., eds. Cambr. Univ. Press, 1985, p. 169\u2013236."},{"key":"21_CR9","unstructured":"Curry H. B., Feys R. Combinatory Logic. vol. 1, North-Holland, 1958."},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Gardner P. Discovering needed reductions using type theory. In: Proc. of TACS'94, Springer LNCS, v. 789, M. Hagiya, J. C. Mitchell, eds. Sendai, 1994, p. 555\u2013574.","DOI":"10.1007\/3-540-57887-0_115"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Glauert J.R.W., Khasidashvili Z. Relative Normalization in Orthogonal Expression Reduction Systems. In: Proc. of CTRS'94, Springer LNCS, vol. 968, N. Dershowitz, N. Lindenstrauss, eds. Jerusalem, 1994, p. 144\u2013165.","DOI":"10.1007\/3-540-60381-6_9"},{"key":"21_CR12","volume-title":"Report SYS-C94-06","author":"J.R.W. Glauert","year":"1994","unstructured":"Glauert J.R.W., Khasidashvili Z. Minimal and optimal relative normalization in Expression Reduction Systems. Report SYS-C94-06, UEA, Norwich, 1994."},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Glauert J.R.W., Khasidashvili Z. Relative normalization in deterministic residual structures. In: Proc. of CAAP'96, Springer LNCS, vol. 1059, H. Kirchner, ed. 1996, p. 180\u2013195.","DOI":"10.1007\/3-540-61064-2_37"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Gonthier G., L\u00e9vy J.-J., Melli\u00e8s P.-A. An abstract Standardisation theorem. In: LICS'92, p. 72\u201381.","DOI":"10.1109\/LICS.1992.185521"},{"key":"21_CR15","unstructured":"Huet G., L\u00e9vy J.-J. Computations in Orthogonal Rewriting Systems. In: Computational Logic, Essays in Honor of Alan Robinson, J.-L. Lassez and G. Plotkin, eds. MIT Press, 1991."},{"key":"21_CR16","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/0168-0072(89)90024-9","volume":"43","author":"J.R. Kennaway","year":"1989","unstructured":"Kennaway J.R. Sequential evaluation strategy for parallel-or and related reduction systems. Annals of Pure and Applied Logic, 43:31\u201356, 1989.","journal-title":"Annals of Pure and Applied Logic"},{"key":"21_CR17","volume-title":"Neededness is hypernormalizing in regular combinatory reduction systems","author":"J. R. Kennaway","year":"1989","unstructured":"Kennaway J. R., Sleep M. R. Neededness is hypernormalizing in regular combinatory reduction systems. Preprint, University of East Anglia, Norwich, 1989."},{"issue":"1","key":"21_CR18","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1006\/inco.1995.1075","volume":"119","author":"J. R. Kennaway","year":"1995","unstructured":"Kennaway J. R., Klop J. W., Sleep M. R., de Vries F.-J. Transfinite reductions in orthogonal term rewriting. Information and Computation, 119(1):18\u201338, 1995.","journal-title":"Information and Computation"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Khasidashvili Z. \u0392-reductions and \u0392-developments of \u03bb-terms with the least number of steps. In: Proc. of the Int. Conference on Computer Logic COLOG'88, Tallinn 1988, Springer LNCS, v. 417, P. Martin-L\u00f6f and G. Mints, eds. 1990, p. 105\u2013111.","DOI":"10.1007\/3-540-52335-9_51"},{"key":"21_CR20","unstructured":"Khasidashvili Z. The Church-Rosser theorem in Orthogonal Combinatory Reduction Systems. Report 1825, INRIA Rocquencourt, 1992."},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Khasidashvili Z. Optimal normalization in orthogonal term rewriting systems. In: Proc. of RTA'93, Springer LNCS, vol. 690, C. Kirchner, ed. Montreal, 1993, p. 243\u2013258.","DOI":"10.1007\/3-540-56868-9_19"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Khasidashvili Z. On higher order recursive program schemes. In: Proc. of CAAP'94, Springer LNCS, vol. 787, S. Tison, ed. Edinburgh, 1994, p. 172\u2013186.","DOI":"10.1007\/BFb0017481"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Khasidashvili Z., van Oostrom V. Context-sensitive conditional expression reduction systems. Electronic Notes in Theoretical Computer Science, vol. 2, A. Corradini, U. Montanari, eds. Elsevier, 1995, p. 141\u2013150.","DOI":"10.1016\/S1571-0661(05)80193-8"},{"key":"21_CR24","volume-title":"Mathematical Centre Tracts n. 127","author":"J. W. Klop","year":"1980","unstructured":"Klop J. W. Combinatory Reduction Systems. Mathematical Centre Tracts n. 127, CWI, Amsterdam, 1980."},{"key":"21_CR25","doi-asserted-by":"crossref","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. In: To Corrado B\u00f6hm, TCS 121:279\u2013308, 1993.","journal-title":"TCS"},{"issue":"1","key":"21_CR26","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0304-3975(76)90009-8","volume":"2","author":"J.-J. L\u00e9vy","year":"1976","unstructured":"L\u00e9vy J.-J. An algebraic interpretation of the \u03bb\u0392K-calculus; and an application of a labelled \u03bb-calculus. TCS 2(1):97\u2013114, 1976.","journal-title":"TCS"},{"key":"21_CR27","unstructured":"L\u00e9vy J.-J. R\u00e9ductions correctes et optimales dans le lambda-calcul, Th\u00e8se de l'Universit\u00e9 de Paris VII, 1978."},{"key":"21_CR28","unstructured":"L\u00e9vy J.-J. Optimal reductions in the Lambda-calculus. In: To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, Hindley J. R., Seldin J. P. eds, Academic Press, 1980, p. 159\u2013192."},{"key":"21_CR29","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/0168-0072(83)90030-1","volume":"24","author":"G. Longo","year":"1983","unstructured":"Longo G. Set theoretic models of lambda calculus: theories, expansions and isomorphisms. Annals of pure and applied logic, 24:153\u2013188, 1983.","journal-title":"Annals of pure and applied logic"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Maranget L. Optimal derivations in weak \u03bb-calculi and in orthogonal Term Rewriting Systems. In: Proc. POPL'91, p. 255\u2013269.","DOI":"10.1145\/99583.99618"},{"key":"21_CR31","unstructured":"Maranget L. La strat\u00e9gie paresseuse. Th\u00e8se de l'Universit\u00e9 de Paris VII, 1992."},{"key":"21_CR32","doi-asserted-by":"crossref","unstructured":"Nipkow T. Orthogonal higher-order rewrite systems are confluent. In: Proc. of TLCA'93, Springer LNCS, vol. 664, Bazem M., Groote J.F., eds., 1993, p. 306\u2013317.","DOI":"10.1007\/BFb0037114"},{"key":"21_CR33","unstructured":"N\u00f6cker E. Efficient Functional Programming. Compilation and Programming Techniques. Ph. D. Thesis, Katholic University of Nijmegen, 1994."},{"key":"21_CR34","unstructured":"Van Oostrom V. Confluence for Abstract and Higher-Order Rewriting. Ph.D. Thesis, Free University of Amsterdam, 1994."},{"key":"21_CR35","doi-asserted-by":"crossref","unstructured":"Van Oostrom V. Higher order families. In proc. of RTA'96, Springer LNCS, vol. 1103, Ganzinger, H., ed., 1996, p. 392\u2013407.","DOI":"10.1007\/3-540-61464-8_67"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Van Oostrom V., van Raamsdonk F. Weak orthogonality implies confluence: the higher-order case. In: Proc. of LFCS'94, Springer LNCS, vol. 813, Narode A., Matiyasevich Yu. V. eds. St. Petersburg, 1994. p. 379\u2013392.","DOI":"10.1007\/3-540-58140-5_35"},{"key":"21_CR37","volume-title":"Ph.D. Thesis","author":"F. Raamsdonk Van","year":"1996","unstructured":"Van Raamsdonk F. Confluence and normalisation for higher-order rewriting. Ph.D. Thesis, CWI Amsterdam, 1996."},{"issue":"1","key":"21_CR38","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1006\/inco.1993.1026","volume":"104","author":"R.C. Sekar","year":"1993","unstructured":"Sekar R.C., Ramakrishnan I.V. Programming in Equational Logic: Beyond Strong Sequentiality. Information and Computation, 104(1):78\u2013109, 1993.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62034-6_53.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:27:43Z","timestamp":1742599663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62034-6_53"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540620341","9783540496311"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-62034-6_53","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}