{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T15:31:58Z","timestamp":1720625518394},"reference-count":21,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2001,12,1]],"date-time":"2001-12-01T00:00:00Z","timestamp":1007164800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":4258,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2001,12]]},"DOI":"10.1016\/s1571-0661(04)00269-5","type":"journal-article","created":{"date-parts":[[2004,2,5]],"date-time":"2004-02-05T10:34:35Z","timestamp":1075977275000},"page":"87-108","source":"Crossref","is-referenced-by-count":4,"special_numbering":"C","title":["Compact Normalisation Trace via Lazy Rewriting"],"prefix":"10.1016","volume":"57","author":[{"given":"Quang-Huy","family":"Nguyen","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB1","unstructured":"C. Alvarado and Q-H. Nguyen. ELAN for equational reasoning in Coq. In J. Despeyroux, editor, Proc. of 2nd Workshop on Logical Frameworks and Metalanguages. Institut National de Recherche en Informatique et en Automatique, ISBN 2\u20137261\u20131166\u20131, June 2000."},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB2","doi-asserted-by":"crossref","unstructured":"S. Antoy. Definitional trees. In H. Kirchner and G. Levi, editors, Proc. of the 3rd International Conference on Algebraic and Logic Programming, volume 632 of Lecture Notes in Computer Science, pages 143\u2013157. Springer-Verlag, September 1992.","DOI":"10.1007\/BFb0013825"},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB3","doi-asserted-by":"crossref","DOI":"10.1142\/S0129054101000412","article-title":"Rewriting with strategies in ELAN: a functional semantics","author":"Borovansk\u00fd","year":"2001","journal-title":"International Journal of Foundations of Computer Science"},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB4","unstructured":"CSL\/SRI. The PVS homepage. http:\/\/pvs.csl.sri.com."},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB5","series-title":"Handbook of Theoretical Computer Science, volume B, chapter 6: Rewrite Systems","first-page":"244","author":"Dershowitz","year":"1990"},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB6","unstructured":"R. Diaconescu and K. Futatsugi. An overview of CafeOBJ. In C. Kirchner and H. Kirchner, editors, Proc. of 2nd International Workshop on Rewriting Logic and its Applications, volume 15 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers B. V. (North-Holland), 2000. Available at http:\/\/www.elsevier.nl\/locate\/volume15.html."},{"issue":"3","key":"10.1016\/S1571-0661(04)00269-5_NEWBIB7","doi-asserted-by":"crossref","first-page":"679","DOI":"10.1145\/291889.291903","article-title":"Within ARM's reach: Compilation of left-linear rewrite systems via minimal rewrite systems","volume":"20","author":"Fokkink","year":"1998","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"10.1016\/S1571-0661(04)00269-5_NEWBIB8","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1145\/345099.345102","article-title":"Lazy rewriting on eager machinery","volume":"2","author":"Fokkink","year":"2000","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB9","series-title":"Software engineering with OBJ, Advances in Formal Methods","article-title":"An introduction to OBJ","author":"Goguen","year":"2000"},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB10","doi-asserted-by":"crossref","unstructured":"A. Graf. Left-to-right tree pattern matching. In Ronald V. Book, editor, Proc. 4th Int. Conf. RTA, volume 488 of Lecture Notes in Computer Science, pages 323\u2013334. Springer-Verlag, 1991.","DOI":"10.1007\/3-540-53904-2_107"},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB11","series-title":"Computational Logic \u2014 Essays in Honor of Alan Robinson","first-page":"395","article-title":"Computations in orthogonal rewriting systems, Part I + II","author":"Huet","year":"1991"},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB12","doi-asserted-by":"crossref","unstructured":"J. Kamperman and P. Walters. Minimal term rewriting systems. In M. Haveraaen, O. Owe, and O. J. Dahl, editors, Recent Trends in Data Type Specification, volume 1130 of Lecture Notes in Computer Science, pages 274\u2013290. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-61629-2_48"},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB13","unstructured":"LogiCal\/INRIA. The Coq homepage. http:\/\/coq.inria.fr."},{"issue":"1","key":"10.1016\/S1571-0661(04)00269-5_NEWBIB14","article-title":"Context-sensitive computations in functional and functional logic programs","volume":"1998","author":"Lucas","year":"1998","journal-title":"Journal of Functional and Logic Programming"},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB15","doi-asserted-by":"crossref","unstructured":"M. Nakamura and K. Ogata. The evaluation strategy for head normal form with and without on-demand flag. In K. Futatsugi, editor, Proc. of 3rd International Workshop on Rewriting Logic and its Applications, volume 36 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers B. V. (North-Holland), 2000. Available at http:\/\/www.elsevier.nl\/locate\/volume36.html.","DOI":"10.1016\/S1571-0661(05)80143-4"},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB16","unstructured":"M.J. O'Donnell. Equational logic programming. In D. Gabbay, editor, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5, Logic Programming, chapter 2. Oxford University Press, 1995. Preprint."},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB17","unstructured":"University of Karlsruhe. The KIV homepage. http:\/\/illwww.ira.uka.de\/~kiv\/KIV-KA.html."},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB18","doi-asserted-by":"crossref","unstructured":"K. Ogata and K. Futatsugi. Operational semantics of rewriting with the on-demand evaluation strategy. In Proc. of ACM Symposium on Applied Computing, pages 756\u2013763, 2000.","DOI":"10.1145\/338407.338558"},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB19","unstructured":"PROTHEO\/LORIA. The ELAN homepage. http:\/\/elan.loria.fr."},{"key":"10.1016\/S1571-0661(04)00269-5_NEWBIB20","doi-asserted-by":"crossref","unstructured":"R I. Strandh. Classes of equational programs that compile into efficient machine code. In N. Dershowitz, editor, Proc. of the 3rd Int. Conf. RTA, volume 355 of Lecture Notes in Computer Science, pages 449\u2013461. Springer-Verlag, April 1989.","DOI":"10.1007\/3-540-51081-8_125"},{"issue":"1","key":"10.1016\/S1571-0661(04)00269-5_NEWBIB21","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1016\/0890-5401(87)90050-2","article-title":"A refinement of strong sequentiality for term rewriting with constructors","volume":"72","author":"Thatte","year":"1987","journal-title":"Information and Computation"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104002695?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104002695?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,30]],"date-time":"2020-03-30T12:28:59Z","timestamp":1585571339000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104002695"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,12]]},"references-count":21,"alternative-id":["S1571066104002695"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00269-5","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2001,12]]}}}