{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:58:39Z","timestamp":1725663519262},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540563938"},{"type":"electronic","value":"9783540475491"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56393-8_36","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T06:08:23Z","timestamp":1330236503000},"page":"448-457","source":"Crossref","is-referenced-by-count":1,"title":["Normalization by leftmost innermost rewriting"],"prefix":"10.1007","author":[{"given":"Sergio","family":"Antoy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"36_CR1","unstructured":"S. Antoy and R. Hamlet. Automatically checking an implementation against its formal specification. In R. Selby, editor, Irvine Software Symposium, pages 29\u201348, Irvine, CA, March 1992."},{"key":"36_CR2","doi-asserted-by":"crossref","unstructured":"Sergio Antoy. Definitional trees. In ALP'92, Volterra, Italy, September 1992. (to appear).","DOI":"10.1007\/BFb0013825"},{"key":"36_CR3","doi-asserted-by":"crossref","unstructured":"Andrew W. Appel and David B. MacQueen. Standard ML of New Jersey. In PLILP'91, pages 1\u201313, Passau, Germany, August 1991. Lect. Notes in Comp. Sci., Vol. 528.","DOI":"10.1007\/3-540-54444-5_83"},{"key":"36_CR4","first-page":"243","volume-title":"Handbook of Theoretical Computer Science B: Formal Methods and Semantics","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 6, pages 243\u2013320. North Holland, Amsterdam, 1990."},{"key":"36_CR5","doi-asserted-by":"crossref","unstructured":"Alfons Geser, Heinrich Hussmann, and Andreas M\u00fcck. A compiler for a class of conditional term rewriting systems. In S. Kaplan and J.-P. Jouannaud, editors, CTRS'87, pages 84\u201390, Orsay, France, July 1987. LNCS 308.","DOI":"10.1007\/3-540-19242-5_7"},{"key":"36_CR6","first-page":"80","volume-title":"Current Trends in Programming Methodology, volume 4","author":"J. A. Goguen","year":"1978","unstructured":"J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the specification, correctness, and implementation of abstract data types. In R. T. Yeh, editor, Current Trends in Programming Methodology, volume 4, pages 80\u2013149. Prentice-Hall, Englewood Cliff, NJ, 1978."},{"key":"36_CR7","volume-title":"Technical Report SRI-CSL-88-9","author":"Joseph A. A. Goguen","year":"1988","unstructured":"Joseph A. Goguen and Timothy Winkler. Introducing OBJ3. Technical Report SRI-CSL-88-9, SRI International, Menlo Park, CA, 1988."},{"key":"36_CR8","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1145\/359605.359618","volume":"20","author":"J. V. Guttag","year":"1977","unstructured":"J. V. Guttag. Abstract data types and the development of data structures. Comm. of the ACM, 20:396\u2013404, 1977.","journal-title":"Comm. of the ACM"},{"key":"36_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69406-6","volume-title":"Fundamentals of Programming Languages","author":"E. Horowitz","year":"1984","unstructured":"Ellis Horowitz. Fundamentals of Programming Languages. Computer Science Press, Rockville, MD, second edition, 1984.","edition":"second edition"},{"key":"36_CR10","first-page":"239","volume":"25","author":"G. Huet","year":"1982","unstructured":"G\u00e9rard Huet and Jean-Marie Hullot. Proofs by induction in equational theories with constructors. JCSS, 25:239\u2013266, 1982.","journal-title":"JCSS"},{"key":"36_CR11","volume-title":"Technical Report 359","author":"G. Huet","year":"1979","unstructured":"G\u00e9rard Huet and Jean-Jacques L\u00e9vy. Call by need computations in non-ambiguous linear term rewriting systems. Technical Report 359, INRIA, Le Chesnay, France, 1979."},{"key":"36_CR12","doi-asserted-by":"crossref","unstructured":"St\u00e9phane Kaplan. A compiler for conditional term rewriting systems. In P. Lescanne, editor, RTA'87, pages 25\u201341, Bordeaux, France, May 1987. LNCS 256.","DOI":"10.1007\/3-540-17220-3_3"},{"key":"36_CR13","doi-asserted-by":"crossref","unstructured":"J. R. Kennaway. The specificity rule for lazy pattern-matching in ambiguous term rewrite systems. In Third European Symp. on Programming, pages 256\u2013270, 1990. LNCS 432.","DOI":"10.1007\/3-540-52592-0_68"},{"key":"36_CR14","doi-asserted-by":"crossref","unstructured":"H. Klaeren and K. Indermark. Efficient implementation of an algebraic specification language. In M. Wirsing and J. A. Bergstra, editors, Algeraic Methods: Theory, Tools and Applications, pages 69\u201390, Passau, Germany, June 1987. LNCS 394.","DOI":"10.1007\/BFb0015036"},{"key":"36_CR15","volume-title":"Technical Report CS-R9073","author":"J. W. Klop","year":"1990","unstructured":"Jan Willem Klop. Term rewriting systems. Technical Report CS-R9073, Stichting Mathematisch Centrum, Amsterdam, The Netherlands, 1990."},{"key":"36_CR16","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1109\/TSE.1986.6312924","volume":"12","author":"J. C. Knight","year":"1986","unstructured":"J. C. Knight and N. G. Leveson. An experimental evaluation of the assumption of independence in multi-version programming. IEEE Trans. on Soft. Eng., 12:96\u2013109, 1986.","journal-title":"IEEE Trans. on Soft. Eng."},{"key":"36_CR17","doi-asserted-by":"crossref","unstructured":"Michael J. O'Donnell. Computing in systems described by equations. Springer-Verlag, 1977. Lect. Notes in Comp. Sci., Vol. 58.","DOI":"10.1007\/3-540-08531-9"},{"key":"36_CR18","doi-asserted-by":"crossref","unstructured":"R. C. Sekar and I. V. Ramakrishnan. Programming in equational logic: Beyond strong sequentiality. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 230\u2013241, Philadelphia, PA, June 1990.","DOI":"10.1109\/LICS.1990.113749"},{"key":"36_CR19","volume-title":"The C++ Programming Language","author":"B. Stroustrup","year":"1986","unstructured":"B. Stroustrup. The C++ Programming Language. Addison-Wesley, Reading, MA, 1986."},{"key":"36_CR20","volume-title":"Master's project","author":"Y. Yan","year":"1992","unstructured":"Yonggong Yan. Building definitional trees. Master's project, Portland Stale University, Portland, OR, March 1992."}],"container-title":["Lecture Notes in Computer Science","Conditional Term Rewriting Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56393-8_36.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,30]],"date-time":"2021-12-30T23:46:45Z","timestamp":1640908005000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56393-8_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540563938","9783540475491"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-56393-8_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}