{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:46:27Z","timestamp":1762458387452},"reference-count":30,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"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":6419,"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":[[1996]]},"DOI":"10.1016\/s1571-0661(04)00037-4","type":"journal-article","created":{"date-parts":[[2004,1,29]],"date-time":"2004-01-29T10:14:39Z","timestamp":1075371279000},"page":"126-148","source":"Crossref","is-referenced-by-count":5,"special_numbering":"C","title":["Reflection and Strategies in Rewriting Logic1 1Supported by Office of Naval Research Contracts N00014-95-C-0225 and N00014-96-C-0114, National Science Foundation Grant CCR-9224005, and by the Information Technology Promotion Agency, Japan, as a part of the Industrial Science and Technology Frontier Program \u201cNew Models for Software Architecture\u201d sponsored by NEDO (New Energy and Industrial Technology Development Organization)."],"prefix":"10.1016","volume":"4","author":[{"given":"Manuel","family":"Clavel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9","family":"Mes eguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB1","unstructured":"William E. Aitken, Robert L. Constable, and Judith L. Underwood. Metalogical frameworks II: Using reflected decision procedures. Technical Report, Computer Sci. Dept., Cornell University, 1993; also, lecture at the Max Planck Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany, July 1993."},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB2","doi-asserted-by":"crossref","unstructured":"Adel Bouhoula, Jean-Pierre Jouannaud, and Jos\u00e9 Meseguer. Specification and proof in membership equational logic. Manuscript, SRI International, August 1996.","DOI":"10.1007\/BFb0030589"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB3","series-title":"The Correctness Problem in Computer Science","first-page":"103","article-title":"Metafunctions: proving them correct and using them efficiently as new proof procedures","author":"Boyer","year":"1981"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB4","doi-asserted-by":"crossref","unstructured":"Manuel Clavel, Steven Eker, Patrick Lincoln, and Jos\u00e9 Meseguer. Principles of Maude. In Jos\u00e9 Meseguer, editor, Proceedings of the first international workshop on rewriting logic, volume 4, Asilomar (California), September 1996. Electronic Notes in Theoretical Computer Science.","DOI":"10.1016\/S1571-0661(04)00034-9"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB5","series-title":"Proceedings of Reflection'96, San Francisco, California, April 1996","first-page":"263","article-title":"Axiomatizing reflective logics and languages","author":"Clavel","year":"1996"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB6","doi-asserted-by":"crossref","unstructured":"Robert L. Constable. Using reflection to explain and enhance type theory. In Helmut Schwichtenberg, editor, Proof and Computation, volume 139 of Computer and System Sciences, pages 109\u2013144. Springer, 1995.","DOI":"10.1007\/978-3-642-79361-5_3"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB7","series-title":"IMSA '92","first-page":"190","article-title":"A system for multi-level reasoning","author":"Giunchiglia","year":"1992"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB8","series-title":"Metatheory and reflection in theorem proving: a survey and critique","author":"Harrison","year":"1995"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB9","series-title":"The G\u00f6del Programming Language","author":"Hill","year":"1994"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB10","series-title":"Proof Theory","first-page":"229","article-title":"Reflecting the semantics of reflected proof","author":"Douglas Howe","year":"1990"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB11","doi-asserted-by":"crossref","unstructured":"Gregor Kiczales, editor. Proceedings of Reflection'96, San Francisco, California, April 1996. Xerox PARC, 1996.","DOI":"10.1145\/239098.239099"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB12","series-title":"The Art of the Metaobject Protocol","author":"Kiczales","year":"1991"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB13","unstructured":"Narciso Mart\u00ed-Oliet and Jos\u00e9 Meseguer. Rewriting logic as a logical and semantic framework. This volume."},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB14","series-title":"What is a Logical System?","first-page":"355","article-title":"General logics and logical frameworks","author":"Mart\u00ed-Oliet","year":"1994"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB15","series-title":"Object-Based Concurrent Computing","first-page":"211","article-title":"Object-oriented concurrent reflective architectures","author":"Matsuoka","year":"1992"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB16","series-title":"In IMSA '92","first-page":"178","article-title":"Reflection in logical systems","author":"Matthews","year":"1992"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB17","first-page":"29","article-title":"Reflection in logic, functional and object-oriented programming: a short comparative study","author":"Demers","year":"1995","journal-title":"IJCAI '95 Workshop on Reflection and Metalevel Architectures and their Applications in AI"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB18","unstructured":"Harald Rue\u00df. Reflection of formal tactics in a deductive reflection framework. Manuscript, Universit\u00e4t Ulm, Abt. K\u00fcnstliche Intelligenz, January 96."},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB19","unstructured":"Jos\u00e9 Meseguer. Membership algebra. Lecture at the Dagstuhl Seminar on \u201cSpecification and Semantics,\u201d July 9, 1996. Extended version in preparation."},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB20","series-title":"Logic Colloquium'87","first-page":"275","article-title":"General logics","author":"\u00e9 Meseguer","year":"1989"},{"issue":"1","key":"10.1016\/S1571-0661(04)00037-4_NEWBIB21","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","article-title":"Conditional rewriting logic as a unified model of concurrency","volume":"96","author":"Meseguer","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB22","series-title":"In IMSA '92","first-page":"36","article-title":"AL-1\/D: A distributed programming system with multi-model reflection framework","author":"Okamura","year":"1992"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB23","series-title":"IMSA '92","first-page":"107","article-title":"A study on the viability of a production-quality metaobject protocol-based statically parallelizing compiler","author":"Luis Rodriguez","year":"1992"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB24","series-title":"Metamathematics, Machines, and G\u00f6del's Proof","author":"Shankar","year":"1994"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB25","unstructured":"Brian Smith and Akinori Yonezawa, editors. Proc. of the IMSA '92 International Workshop on Reflection and Meta-Level Architecture, Tokyo, November 1992. Research Institute of Software Engineering, 1992."},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB26","doi-asserted-by":"crossref","unstructured":"Brian C. Smith. Reflection and Semantics in Lisp. In Proc. POPL'84, pages 23\u201335. ACM, 1984.","DOI":"10.1145\/800017.800513"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB27","unstructured":"G. L. Steele, Jr. and G. J. Sussman. The art of the interpreter or, the modularity complex. Technical Report AIM-453, MIT AI-Lab, May 1978."},{"issue":"3","key":"10.1016\/S1571-0661(04)00037-4_NEWBIB28","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1145\/5956.5957","article-title":"The concept of a supercompiler","volume":"8","author":"Valentin Turchin","year":"1986","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"10.1016\/S1571-0661(04)00037-4_NEWBIB29","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/BF01806174","article-title":"The mystery of the tower revealed","volume":"1","author":"Wand","year":"1988","journal-title":"Lisp and Symbolic Computation"},{"key":"10.1016\/S1571-0661(04)00037-4_NEWBIB30","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0004-3702(80)90015-6","article-title":"Prolegomena to a theory of mechanized formal reasoning","volume":"13","author":"Richard Weyhrauch","year":"1980","journal-title":"Artificial Intelligence"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104000374?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104000374?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,29]],"date-time":"2020-03-29T12:32:15Z","timestamp":1585485135000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104000374"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"references-count":30,"alternative-id":["S1571066104000374"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00037-4","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[1996]]}}}