{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:37:57Z","timestamp":1725489477749},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540414131"},{"type":"electronic","value":"9783540444503"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44450-5_4","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T08:26:08Z","timestamp":1187252768000},"page":"55-80","source":"Crossref","is-referenced-by-count":8,"title":["Rewriting Logic as a Metalogical Framework"],"prefix":"10.1007","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[]},{"given":"Manuel","family":"Clavel","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,11,24]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"P. Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of Mathematical Logic, pages 739\u2013782. North-Holland, Amsterdam, 1977.","key":"4_CR1","DOI":"10.1016\/S0049-237X(08)71120-0"},{"doi-asserted-by":"crossref","unstructured":"D. Basin, M. Clavel, and J. Meseguer. Rewriting logic as a metalogical framework. Technical report, September 2000, http:\/\/maude.csl.sri.com .","key":"4_CR2","DOI":"10.1007\/3-540-44450-5_4"},{"unstructured":"D. Basin and R. Constable. Metalogical frameworks. In G. Huet and G. Plotkin, editors, Logical Environments, pages 1\u201329. Cambridge University Press, 1993.","key":"4_CR3"},{"doi-asserted-by":"crossref","unstructured":"D. Basin and S. Matthews. Scoped metatheorems. In International Workshop on Rewriting Logic and its Applications, volume 15, pages 1\u201312. Electronic Notes in Theoretical Computer Science (ENTCS), September 1998.","key":"4_CR4","DOI":"10.1016\/S1571-0661(05)80021-0"},{"doi-asserted-by":"crossref","unstructured":"D. Basin and S. Matthews. Structuring metatheory on inductive definitions. Information and Computation, 2000. To appear.","key":"4_CR5","DOI":"10.1006\/inco.2000.2858"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/S0304-3975(99)00206-6","volume":"236","author":"A. Bouhoula","year":"2000","unstructured":"A. Bouhoula, J.-P. Jouannaud, and J. Meseguer. Specification and proof in membership equational logic. Theoretical Computer Science, 236:35\u2013132, 2000.","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"M. Clavel. Reflection in General Logics and in Rewriting Logic with Applications to the Maude Language. PhD thesis, University of Navarre, 1998.","key":"4_CR7","DOI":"10.1016\/S1571-0661(05)82553-8"},{"doi-asserted-by":"crossref","unstructured":"M. Clavel, F. Dur\u00e1n, S. Eker, P. Lincoln, N. Mart\u00ed-Oliet, and J. Meseguer. Metalevel computation in Maude. In C. Kirchner and H. Kirchner, editors, Second International Workshop on Rewriting Logic and its Applications, volume 15 of Electronic Notes in Theoretical Computer Science, pages 3-23, Pont-\u00e1-Mousson, France, September 1998. sevier.","key":"4_CR8","DOI":"10.1016\/S1571-0661(05)80020-9"},{"unstructured":"M. Clavel, F. Dur\u00e1n, S. Eker, P. Lincoln, N. Mart\u00ed-Oliet, J. Meseguer, and J. Quesada. Maude: Specification and programming in rewriting logic. SRI International, January 1999, http:\/\/maude.csl.sri.com .","key":"4_CR9"},{"unstructured":"M. Clavel, F. Dur\u00e1n, S. Eker, and J. Meseguer. Building equational proving tools by reflection in rewriting logic. In Proceedings of the CafeOBJ Symposium\u2019 98, Numazu, Japan. CafeOBJ Project, April 1998.","key":"4_CR10"},{"key":"4_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1684","DOI":"10.1007\/3-540-48118-4_39","volume-title":"FM\u201999\u2019 Formal Methods","author":"M. Clavel","year":"1999","unstructured":"M. Clavel, F. Dur\u00e1n, S. Eker, J. Meseguer, and M.-O. Stehr. Maude as a formal meta-tool. In J. Wing and J. Woodcock, editors, FM\u201999\u2019 Formal Methods, volume 1709 of Lecture Notes in Computer Science, pages 1684\u20131703. Springer-Verlag, 1999."},{"doi-asserted-by":"crossref","unstructured":"M. Clavel, F. Dur\u00e1n, and N. Mart\u00ed-Oliet. Polytypic programming in Maude. To appear in Proc. WRLA 2000, ENTCS, Elsevier, 2000.","key":"4_CR12","DOI":"10.1007\/3-540-46428-X_27"},{"doi-asserted-by":"crossref","unstructured":"M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In J. Meseguer, editor, First International Workshop on Rewriting Logic and its Applications, volume 4 of Electronic Notes in Theoretical Computer Science, pages 65\u201389, Asilomar (California), September 1996. Elsevier.","key":"4_CR13","DOI":"10.1016\/S1571-0661(04)00034-9"},{"unstructured":"M. Clavel and J. Meseguer. Axiomatizing reflective logics and languages. In G. Kiczales, editor, Proceedings of Reflection\u201996, pages 263\u2013288, San Francisco (California), April 1996. Xerox PARC.","key":"4_CR14"},{"unstructured":"M. Clavel and J. Meseguer. Reflection and strategies in rewriting logic. In J. Meseguer, editor, First International Workshop on Rewriting Logic and its Applications, volume 4 of Electronic Notes in Theoretical Computer Science, pages 125\u2013147, Asilomar (California), September 1996. Elsevier.","key":"4_CR15"},{"unstructured":"M. Clavel and J. Meseguer. Reflection in condition rewriting logic. Manuscript.Submitted for publication, 2000.","key":"4_CR16"},{"key":"4_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Primitive recursion for higherorder abstract syntax","author":"J. Despeyroux","year":"1997","unstructured":"J. Despeyroux, F. Pfenning, and C. Sch\u00fcrmann. Primitive recursion for higherorder abstract syntax. In Proceedings of the 3rd International Conference on Typed Lambda Calculi and Applications (TLCA\u201997), volume 1210 ofLecture Notes in Computer Science, Nancy, France, April 1997. Springer-Verlag."},{"unstructured":"F. Dur\u00e1n. A Reflective Module Algebra with Applications to the Maude Language. PhD thesis, University of M\u00e1laga, 1999.","key":"4_CR18"},{"doi-asserted-by":"crossref","unstructured":"S. Feferman. Finitary inductively presented logics. In Logic Colloquium\u2019 88. North-Holland, 1988.","key":"4_CR19","DOI":"10.1016\/S0049-237X(08)70270-2"},{"key":"4_CR20","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Models and equality for logical programming","author":"J. Goguen","year":"2001","unstructured":"J. Goguen and J. Meseguer. Models and equality for logical programming. In H. Ehrig, G. Levi, R. Kowalski, and U. Montanari, editors, Proceedings TAPSOFT\u2019 87, volume 250 of Lecture Notes in Computer Science, pages 1\u201322. Springer-Verlag, 1987."},{"unstructured":"M. Gordon and T. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.","key":"4_CR21"},{"issue":"1","key":"4_CR22","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. J. ACM, 40(1):143\u2013184, January 1993.","journal-title":"J. ACM"},{"unstructured":"N. Mart\u00ed-Oliet and J. Meseguer. Rewriting logic as a logical and semantic framework. Technical Report SRI-CSL-93-05, SRI International, Computer Science Laboratory, August 1993. To appear in D. Gabbay, ed., Handbook of Philosophical Logic, Kluwer Academic Publishers.","key":"4_CR23"},{"doi-asserted-by":"crossref","unstructured":"N. Mart\u00ed-Oliet and J. Meseguer. General logics and logical frameworks. In D. Gabbay, editor, What is a Logical System?, pages 355\u2013392. Oxford University Press, 1994.","key":"4_CR24","DOI":"10.1093\/oso\/9780198538592.003.0014"},{"unstructured":"S. Matthews, A. Smaill, and D. Basin. Experience with FS0 as a framework theory. In G. Huet and G. Plotkin, editors, Logical Environments, pages 61\u201382. Cambridge University Press, 1993.","key":"4_CR25"},{"doi-asserted-by":"crossref","unstructured":"R. McDowell and D. Miller. A logic for reasoning with higher-order abstract syntax. In Twelfth Annual IEEE Symposium on Logic in Computer Science, June 1997.","key":"4_CR26","DOI":"10.1109\/LICS.1997.614968"},{"doi-asserted-by":"crossref","unstructured":"J. Meseguer. General logics. In H.-D. Ebbinghaus et al., editor, Logic Colloquium\u2019 87, pages 275\u2013329. North-Holland, 1989.","key":"4_CR27","DOI":"10.1016\/S0049-237X(08)70132-0"},{"issue":"1","key":"4_CR28","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73\u2013155, 1992.","journal-title":"Theoretical Computer Science"},{"key":"4_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Membership algebra as a semantic framework for equational specification","author":"J. Meseguer","year":"1998","unstructured":"J. Meseguer. Membership algebra as a semantic framework for equational specification. In F. Parisi-Presicce, editor, Proceedings of WADT\u201997, volume 1376 of Lecture Notes in Computer Science, pages 18\u201361. Springer-Verlag, 1998."},{"doi-asserted-by":"crossref","unstructured":"J. Meseguer. Research directions in rewriting logic. In U. Berger and H. Schwichtenberg, editors, Computational Logic, NATO Advanced Study Institute, Marktoberdorf, Germany, July 29-August 6, 1997. Springer-Verlag, 1998.","key":"4_CR30","DOI":"10.1007\/978-3-642-58622-4_10"},{"unstructured":"J. Meseguer and J. A. Goguen. Initiality, induction and computability. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, pages 459\u2013541. Cambridge University Press, 1985.","key":"4_CR31"},{"key":"4_CR32","series-title":"Lect Notes Comput Sci","volume-title":"Inductive Definitions in the System Coq\u2019 Rules and Properties","author":"C. Paulin-Mohring","year":"1993","unstructured":"C. Paulin-Mohring. Inductive Definitions in the System Coq\u2019 Rules and Properties. In M. Bezem and J.-F. Groote, editors, Proceedings of the conference Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, 1993."},{"doi-asserted-by":"crossref","unstructured":"L. C. Paulson. A fixedpoint approach to implementing (co)inductive definitions. In Proceedings of the 12th International Conference on Automated Deduction (CADE-12), volume 814 of Lecture Notes in Artificial Intelligence, Nancy, France, June 1994. Springer-Verlag.","key":"4_CR33","DOI":"10.1007\/3-540-58156-1_11"},{"key":"4_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: a generic theorem prover; with contributions by Tobias Nipkow","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle: a generic theorem prover; with contributions by Tobias Nipkow, volume 828 of Lecture Notes in Computer Science. Springer, Berlin, 1994."},{"key":"4_CR35","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/BFb0054266","volume-title":"Automated theorem proving in a simple metalogic for LF","author":"C. Sch\u00fcrmann","year":"1998","unstructured":"C. Sch\u00fcrmann and F. Pfenning. Automated theorem proving in a simple metalogic for LF. In C. Kirchner and H. Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction (CADE-15), volume 1421 of Lecture Notes in Computer Science, pages 286\u2013300, Lindau, Germany, July 1998. Springer-Verlag."},{"unstructured":"M.-O. Stehr and J. Meseguer. Pure type systems in rewriting logic. In Proc. of LFM\u201999: Workshop on Logical Frameworks and Meta-languages, 1999. http:\/\/www.cs.bell-labs.com\/~felty\/LFM99\/ .","key":"4_CR36"},{"unstructured":"M.-O. Stehr, P. Naumov, and J. Meseguer. A proof-theoretic approach to the HOL-Nuprl connection with applications to proof translation. Manuscript, SRI International, http:\/\/www.csl.sri.com\/~stehr\/fi_eng.html , February 2000.","key":"4_CR37"},{"key":"4_CR38","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/321978.321991","volume":"23","author":"M. Emden van","year":"1976","unstructured":"M. van Emden and R. Kowalski. The semantics of predicate logic as a programming language. J. ACM, 23:733\u201342, 1976.","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44450-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,17]],"date-time":"2024-02-17T12:12:19Z","timestamp":1708171939000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44450-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540414131","9783540444503"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-44450-5_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}