{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T22:57:27Z","timestamp":1765666647594,"version":"3.41.0"},"reference-count":76,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2004,7,1]],"date-time":"2004-07-01T00:00:00Z","timestamp":1088640000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2004,7]]},"abstract":"<jats:p>A metalogical framework is a logic with an associated methodology that is used to represent other logics and to reason about their metalogical properties. We propose that logical frameworks can be good metalogical frameworks when their theories always have initial models and they support reflective and parameterized reasoning.We develop this thesis both abstractly and concretely. Abstractly, we formalize our proposal as a set of requirements and explain how any logic satisfying these requirements can be used for metalogical reasoning. Concretely, we present membership equational logic as a particular metalogic that satisfies these requirements. Using membership equational logic, and its realization in the Maude system, we show how reflection can be used for different, nontrivial kinds of formal metatheoretic reasoning. In particular, one can prove metatheorems that relate theories or establish properties of parameterized classes of theories.<\/jats:p>","DOI":"10.1145\/1013560.1013566","type":"journal-article","created":{"date-parts":[[2004,10,7]],"date-time":"2004-10-07T17:38:56Z","timestamp":1097170736000},"page":"528-576","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Reflective metalogical frameworks"],"prefix":"10.1145","volume":"5","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manuel","family":"Clavel","sequence":"additional","affiliation":[{"name":"Universidad Complutense de Madrid, Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, IL"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2004,7]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Eds","author":"Abramson H.","year":"1989","unstructured":"Abramson , H. and Rogers , M. , Eds . 1989 . Metaprogramming in Logic Programming. MIT Press , Cambridge, MA.]] Abramson, H. and Rogers, M., Eds. 1989. Metaprogramming in Logic Programming. MIT Press, Cambridge, MA.]]"},{"volume-title":"Handbook of Mathematical Logic","author":"Aczel P.","key":"e_1_2_1_2_1","unstructured":"Aczel , P. 1977. An introduction to inductive definitions . In Handbook of Mathematical Logic , J. Barwise, Ed. North-Holland, Amsterdam , The Netherlands , 739--782.]] Aczel, P. 1977. An introduction to inductive definitions. In Handbook of Mathematical Logic, J. Barwise, Ed. North-Holland, Amsterdam, The Netherlands, 739--782.]]"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005929703675"},{"volume-title":"Symposium on Logic in Computer Science. IEEE Computer Society Press","author":"Allen S. F.","key":"e_1_2_1_4_1","unstructured":"Allen , S. F. , Constable , R. L. , Howe , D. J. , and Aitken , W . 1990. The semantics of reflected proof . In Symposium on Logic in Computer Science. IEEE Computer Society Press , Los Alamitos, CA.]] Allen, S. F., Constable, R. L., Howe, D. J., and Aitken, W. 1990. The semantics of reflected proof. In Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA.]]"},{"key":"e_1_2_1_5_1","volume-title":"Eds","author":"Apt K.","year":"1995","unstructured":"Apt , K. and Turini , F. , Eds . 1995 . Meta-Logics and Logic Programming. Logic Programming Series. MIT Press , Cambridge, MA.]] Apt, K. and Turini, F., Eds. 1995. Meta-Logics and Logic Programming. Logic Programming Series. MIT Press, Cambridge, MA.]]"},{"key":"e_1_2_1_6_1","unstructured":"Basin D. and Constable R. 1993. Metalogical frameworks. In Logical Environments G. Huet and G. Plotkin Eds. Cambridge University Press Cambridge MA 1--29.]] Basin D. and Constable R. 1993. Metalogical frameworks. In Logical Environments G. Huet and G. Plotkin Eds. Cambridge University Press Cambridge MA 1--29.]]"},{"key":"e_1_2_1_7_1","volume-title":"Second International Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science","volume":"15","author":"Basin D.","unstructured":"Basin , D. and Matthews , S . 1998. Scoped metatheorems . In Second International Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science , vol. 15 . Elsevier, Amsterdam, The Netherlands, 1--12.]] Basin, D. and Matthews, S. 1998. Scoped metatheorems. In Second International Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 15. Elsevier, Amsterdam, The Netherlands, 1--12.]]"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.2000.2858","article-title":"Structuring metatheory on inductive definitions","volume":"162","author":"Basin D.","year":"2000","unstructured":"Basin , D. and Matthews , S. 2000 . Structuring metatheory on inductive definitions . Inform. Computat. 162 , 1 -- 2 (Oct.\/Nov.), 80--95.]] Basin, D. and Matthews, S. 2000. Structuring metatheory on inductive definitions. Inform. Computat. 162, 1--2 (Oct.\/Nov.), 80--95.]]","journal-title":"Inform. Computat."},{"key":"e_1_2_1_9_1","unstructured":"Basin D. and Matthews S. 2002. Logical frameworks. In Handbook of Philosophical Logic 2nd ed. vol. 9 D. Gabbay and F. Guenthner Eds. Kluwer Academic Publishers Dordrecht The Netherlands 89--164.]] Basin D. and Matthews S. 2002. Logical frameworks. In Handbook of Philosophical Logic 2nd ed. vol. 9 D. Gabbay and F. Guenthner Eds. Kluwer Academic Publishers Dordrecht The Netherlands 89--164.]]"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00206-6"},{"key":"e_1_2_1_11_1","volume-title":"Metafunctions: Proving them correct and using them efficiently as new proof procedures. In The Correctness Problem in Computer Science","author":"Boyer R. S.","year":"1981","unstructured":"Boyer , R. S. and Moore , J. S . 1981 . Metafunctions: Proving them correct and using them efficiently as new proof procedures. In The Correctness Problem in Computer Science , R. S. Boyer and J. S. Moore, Eds. Academic Press , New York, NY , 103--185.]] Boyer, R. S. and Moore, J. S. 1981. Metafunctions: Proving them correct and using them efficiently as new proof procedures. In The Correctness Problem in Computer Science, R. S. Boyer and J. S. Moore, Eds. Academic Press, New York, NY, 103--185.]]"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings Second Workshop on Meta-Programming in Logic. K. U. Leuven","author":"Bruynooghe M., Ed.","year":"1990","unstructured":"Bruynooghe , M., Ed. 1990 . Proceedings Second Workshop on Meta-Programming in Logic. K. U. Leuven , Leuven, Belgium.]] Bruynooghe, M., Ed. 1990. Proceedings Second Workshop on Meta-Programming in Logic. K. U. Leuven, Leuven, Belgium.]]"},{"volume-title":"Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications","author":"Clavel M.","key":"e_1_2_1_13_1","unstructured":"Clavel , M. 2000. Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications , CSLI Publications , Stanford, CA .]] Clavel, M. 2000. Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications, CSLI Publications, Stanford, CA.]]"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00359-0"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Clavel M. Dur\u00e1n F. Eker S. and Meseguer J. 2000a. Building equational proving tools by reflection in rewriting logic. In CAFE: An Industrial-Strength Algebraic Formal Method K. Futatsugi A. T. Nakagawa and T. Tamai Eds. Elsevier Amsterdam The Netherlands 1--31.]] Clavel M. Dur\u00e1n F. Eker S. and Meseguer J. 2000a. Building equational proving tools by reflection in rewriting logic. In CAFE: An Industrial-Strength Algebraic Formal Method K. Futatsugi A. T. Nakagawa and T. Tamai Eds. Elsevier Amsterdam The Netherlands 1--31.]]","DOI":"10.1016\/B978-044450556-9\/50061-7"},{"key":"e_1_2_1_16_1","volume-title":"-O","author":"Clavel M.","year":"1999","unstructured":"Clavel , M. , Dur\u00e1n , F. , Eker , S. , Meseguer , J. , and Stehr , M . -O . 1999 . Maude as a formal meta-tool. In FM'99---Formal Methods, J. Wing and J. Woodcock, Eds. Lecture Notes in Computer Science, vol. 1709 . Springer-Verlag , Berlin, Germany, 1684--1703.]] Clavel, M., Dur\u00e1n, F., Eker, S., Meseguer, J., and Stehr, M.-O. 1999. Maude as a formal meta-tool. In FM'99---Formal Methods, J. Wing and J. Woodcock, Eds. Lecture Notes in Computer Science, vol. 1709. Springer-Verlag, Berlin, Germany, 1684--1703.]]"},{"key":"e_1_2_1_17_1","volume-title":"Third International Workshop on Rewriting Logic and its Applications, K. Futatsugi, Ed. Electronic Notes in Theoretical Computer Science","volume":"36","author":"Clavel M.","unstructured":"Clavel , M. , Dur\u00e1n , F. , and Mart\u00ed-Oliet , N . 2000b. Polytypic programming in Maude . In Third International Workshop on Rewriting Logic and its Applications, K. Futatsugi, Ed. Electronic Notes in Theoretical Computer Science , vol. 36 . Elsevier, Amsterdam, The Netherlands, 339--360.]] Clavel, M., Dur\u00e1n, F., and Mart\u00ed-Oliet, N. 2000b. Polytypic programming in Maude. In Third International Workshop on Rewriting Logic and its Applications, K. Futatsugi, Ed. Electronic Notes in Theoretical Computer Science, vol. 36. Elsevier, Amsterdam, The Netherlands, 339--360.]]"},{"key":"e_1_2_1_18_1","volume-title":"Principles of Maude. In First International Workshop on Rewriting Logic and its Applications, J. Meseguer, Ed. Electronic Notes in Theoretical Computer Science","volume":"4","author":"Clavel M.","unstructured":"Clavel , M. , Eker , S. , Lincoln , P. , and Meseguer , J . 1996 . Principles of Maude. In First International Workshop on Rewriting Logic and its Applications, J. Meseguer, Ed. Electronic Notes in Theoretical Computer Science , vol. 4 . Elsevier, Amsterdam, The Netherlands, 65--89.]] Clavel, M., Eker, S., Lincoln, P., and Meseguer, J. 1996. Principles of Maude. In First International Workshop on Rewriting Logic and its Applications, J. Meseguer, Ed. Electronic Notes in Theoretical Computer Science, vol. 4. Elsevier, Amsterdam, The Netherlands, 65--89.]]"},{"volume-title":"Proceedings of the 10th International Conference on Algebraic Methodology and Software Technology (AMAST'04)","author":"Clavel M.","key":"e_1_2_1_19_1","unstructured":"Clavel , M. , Mart\u00ed-Oliet , N. , and Palomino , M . 2004. Formalizing and proving semantics relations between specifications by reflection . In Proceedings of the 10th International Conference on Algebraic Methodology and Software Technology (AMAST'04) , Stirling, UK.]] Clavel, M., Mart\u00ed-Oliet, N., and Palomino, M. 2004. Formalizing and proving semantics relations between specifications by reflection. In Proceedings of the 10th International Conference on Algebraic Methodology and Software Technology (AMAST'04), Stirling, UK.]]"},{"volume-title":"Proceedings of Reflection'96","author":"Clavel M.","key":"e_1_2_1_20_1","unstructured":"Clavel , M. and Meseguer , J . 1996. Axiomatizing reflective logics and languages . In Proceedings of Reflection'96 , G. Kiczales, Ed. Xerox PARC, San Francisco, CA, 263--288.]] Clavel, M. and Meseguer, J. 1996. Axiomatizing reflective logics and languages. In Proceedings of Reflection'96, G. Kiczales, Ed. Xerox PARC, San Francisco, CA, 263--288.]]"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00360-7"},{"key":"e_1_2_1_22_1","volume-title":"Fourth International Workshop on Rewriting Logic and its Applications, F. Gadducci and U. Montanari, Eds. Electronic Notes in Theoretical Computer Science","volume":"71","author":"Clavel M.","unstructured":"Clavel , M. , Meseguer , J. , and Palomino , M . 2002b. Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic . In Fourth International Workshop on Rewriting Logic and its Applications, F. Gadducci and U. Montanari, Eds. Electronic Notes in Theoretical Computer Science , vol. 71 . Elsevier, Amsterdam, The Netherlands, 63--78.]] Clavel, M., Meseguer, J., and Palomino, M. 2002b. Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic. In Fourth International Workshop on Rewriting Logic and its Applications, F. Gadducci and U. Montanari, Eds. Electronic Notes in Theoretical Computer Science, vol. 71. Elsevier, Amsterdam, The Netherlands, 63--78.]]"},{"key":"e_1_2_1_23_1","series-title":"Lecture Notes in Computer Science","volume-title":"1999. Proceedings of Reflection'99","author":"Cointe P.","unstructured":"Cointe , P. , Ed. 1999. Proceedings of Reflection'99 . Lecture Notes in Computer Science , vol. 1616 . Springer-Verlag , Berlin, Germany .]] Cointe, P., Ed. 1999. Proceedings of Reflection'99. Lecture Notes in Computer Science, vol. 1616. Springer-Verlag, Berlin, Germany.]]"},{"volume-title":"Computer and System Sciences","author":"Constable R. L.","key":"e_1_2_1_24_1","unstructured":"Constable , R. L. 1995. Using reflection to explain and enhance type theory . In Proof and Computation, H. Schwichtenberg, Ed. Computer and System Sciences , vol. 139 . Springer-Verlag , Berlin, Germany , 109--144.]] Constable, R. L. 1995. Using reflection to explain and enhance type theory. In Proof and Computation, H. Schwichtenberg, Ed. Computer and System Sciences, vol. 139. Springer-Verlag, Berlin, Germany, 109--144.]]"},{"volume-title":"Proceedings of IJCAI'95---Workshop on Reflection and Metalevel Architectures and their Applications in AI. 29--38","author":"Demers F.-N.","key":"e_1_2_1_25_1","unstructured":"Demers , F.-N. and Malenfant , J . 1995. Reflection in logic, functional and object-oriented programming: A short comparative study . In Proceedings of IJCAI'95---Workshop on Reflection and Metalevel Architectures and their Applications in AI. 29--38 .]] Demers, F.-N. and Malenfant, J. 1995. Reflection in logic, functional and object-oriented programming: A short comparative study. In Proceedings of IJCAI'95---Workshop on Reflection and Metalevel Architectures and their Applications in AI. 29--38.]]"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the 3rd International Conference on Typed Lambda Calculi and Applications (TLCA'97)","volume":"1210","author":"Despeyroux J.","unstructured":"Despeyroux , J. , Pfenning , F. , and Sch\u00fcrmann , C . 1997. Primitive recursion for higher-order abstract syntax . In Proceedings of the 3rd International Conference on Typed Lambda Calculi and Applications (TLCA'97) (Nancy, France). Lecture Notes in Computer Science , vol. 1210 . Springer-Verlag, Berlin, Germany.]] Despeyroux, J., Pfenning, F., and Sch\u00fcrmann, C. 1997. Primitive recursion for higher-order abstract syntax. In Proceedings of the 3rd International Conference on Typed Lambda Calculi and Applications (TLCA'97) (Nancy, France). Lecture Notes in Computer Science, vol. 1210. Springer-Verlag, Berlin, Germany.]]"},{"key":"e_1_2_1_28_1","volume-title":"EATCS Monographs on Theoretical Computer Science","volume":"6","author":"Ehrig H.","unstructured":"Ehrig , H. and Mahr , B . 1985. Fundamentals of Algebraic Specification 1 . EATCS Monographs on Theoretical Computer Science , vol. 6 . Springer-Verlag, Berlin, Germany.]] Ehrig, H. and Mahr, B. 1985. Fundamentals of Algebraic Specification 1. EATCS Monographs on Theoretical Computer Science, vol. 6. Springer-Verlag, Berlin, Germany.]]"},{"key":"e_1_2_1_29_1","volume-title":"Logic Colloquium '88","author":"Feferman S.","year":"1988","unstructured":"Feferman , S. 1988 . Finitary inductively presented logics . In Logic Colloquium '88 . North-Holland, Amsterdam, The Netherlands, 191--220.]] Feferman, S. 1988. Finitary inductively presented logics. In Logic Colloquium '88. North-Holland, Amsterdam, The Netherlands, 191--220.]]"},{"key":"e_1_2_1_30_1","volume-title":"Eds","author":"Fribourg L.","year":"1994","unstructured":"Fribourg , L. and Turini , F. , Eds . 1994 . Logic Program Synthesis and Transformation--Meta-programming in Logic. Lecture Notes in Computer Science, vol. 883 . Springer-Verlag , Berlin, Germany.]] Fribourg, L. and Turini, F., Eds. 1994. Logic Program Synthesis and Transformation--Meta-programming in Logic. Lecture Notes in Computer Science, vol. 883. Springer-Verlag, Berlin, Germany.]]"},{"volume-title":"IMSA'92---International Workshop on Reflection and Meta-Level Architecture. Information-Technology Promotion Agency","author":"Giunchiglia F.","key":"e_1_2_1_32_1","unstructured":"Giunchiglia , F. , Traverso , P. , Cimatti , A. , and Pecchiari , P . 1992. A system for multi-level reasoning . In IMSA'92---International Workshop on Reflection and Meta-Level Architecture. Information-Technology Promotion Agency , Tokyo, Japan, 190--195.]] Giunchiglia, F., Traverso, P., Cimatti, A., and Pecchiari, P. 1992. A system for multi-level reasoning. In IMSA'92---International Workshop on Reflection and Meta-Level Architecture. Information-Technology Promotion Agency, Tokyo, Japan, 190--195.]]"},{"key":"e_1_2_1_33_1","volume-title":"Logic of Programming Workshop, E. Clarke and D. Kozen, Eds. Lecture Notes in Computer Science","volume":"164","author":"Goguen J.","unstructured":"Goguen , J. and Burstall , R . 1984. Introducing institutions . In Logic of Programming Workshop, E. Clarke and D. Kozen, Eds. Lecture Notes in Computer Science , vol. 164 . Springer-Verlag, Berlin, Germany, 221--256.]] Goguen, J. and Burstall, R. 1984. Introducing institutions. In Logic of Programming Workshop, E. Clarke and D. Kozen, Eds. Lecture Notes in Computer Science, vol. 164. Springer-Verlag, Berlin, Germany, 221--256.]]"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/147508.147524"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of TAPSOFT'87","volume":"250","author":"Goguen J.","unstructured":"Goguen , J. and Meseguer , J . 1987. Models and equality for logical programming . In Proceedings of TAPSOFT'87 , H. Ehrig, G. Levi, R. Kowalski, and U. Montanari, Eds. Lecture Notes in Computer Science , vol. 250 . Springer-Verlag, Berlin, Germany, 1--22.]] Goguen, J. and Meseguer, J. 1987. Models and equality for logical programming. In Proceedings of TAPSOFT'87, H. Ehrig, G. Levi, R. Kowalski, and U. Montanari, Eds. Lecture Notes in Computer Science, vol. 250. Springer-Verlag, Berlin, Germany, 1--22.]]"},{"key":"e_1_2_1_36_1","volume-title":"HOL: A Theorem Proving Environment for Higher Order Logic","author":"Gordon M.","year":"1993","unstructured":"Gordon , M. and Melham , T . 1993 . Introduction to HOL: A Theorem Proving Environment for Higher Order Logic . Cambridge University Press, Cambridge , U.K. ]] Gordon, M. and Melham, T. 1993. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge, U.K.]]"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_2_1_39_1","unstructured":"Hill P. and Lloyd J. 1989. Analysis of meta-programs. In Meta-Programming in Logic Programming H. D. Abramson and M. H. Rogers Eds. MIT Press Cambridge MA 23--52.]] Hill P. and Lloyd J. 1989. Analysis of meta-programs. In Meta-Programming in Logic Programming H. D. Abramson and M. H. Rogers Eds. MIT Press Cambridge MA 23--52.]]"},{"key":"e_1_2_1_40_1","unstructured":"Hill P. and Lloyd J. 1994. The G\u00f6del Programming Language. MIT Press Cambridge MA.]] Hill P. and Lloyd J. 1994. The G\u00f6del Programming Language. MIT Press Cambridge MA.]]"},{"key":"e_1_2_1_41_1","volume-title":"9th International Conference on Automated Deduction","volume":"310","author":"Howe D. J.","year":"1988","unstructured":"Howe , D. J. 1988 . Computational metatheory in Nuprl . In 9th International Conference on Automated Deduction ( Argonne, IL). Lecture Notes in Computer Science , vol. 310 . Springer-Verlag, Berlin, Germany, 238--257.]] Howe, D. J. 1988. Computational metatheory in Nuprl. In 9th International Conference on Automated Deduction (Argonne, IL). Lecture Notes in Computer Science, vol. 310. Springer-Verlag, Berlin, Germany, 238--257.]]"},{"volume-title":"Cambridge University Press","author":"Howe D. J.","key":"e_1_2_1_42_1","unstructured":"Howe , D. J. 1990. Reflecting the semantics of reflected proof . In Proof Theory, P. Aczel, H. Simmons, and S. Wainer, Eds. Cambridge University Press , Cambridge , U.K. , 229--250.]] Howe, D. J. 1990. Reflecting the semantics of reflected proof. In Proof Theory, P. Aczel, H. Simmons, and S. Wainer, Eds. Cambridge University Press, Cambridge, U.K., 229--250.]]"},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the Second International Summer School on Advanced Functional Programming Techniques, J. Launchbury, E. Meijer, and T. Sheard, Eds. Lecture Notes in Computer Science","volume":"1129","author":"Jeuring J.","unstructured":"Jeuring , J. and Jansson , P . 1996. Polytypic programming . In Proceedings of the Second International Summer School on Advanced Functional Programming Techniques, J. Launchbury, E. Meijer, and T. Sheard, Eds. Lecture Notes in Computer Science , vol. 1129 . Springer-Verlag, Berlin, Germany, 68--114.]] Jeuring, J. and Jansson, P. 1996. Polytypic programming. In Proceedings of the Second International Summer School on Advanced Functional Programming Techniques, J. Launchbury, E. Meijer, and T. Sheard, Eds. Lecture Notes in Computer Science, vol. 1129. Springer-Verlag, Berlin, Germany, 68--114.]]"},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of Reflection'96","author":"Kiczales G., Ed.","year":"1996","unstructured":"Kiczales , G., Ed. 1996 . Proceedings of Reflection'96 , G. Kiczales, ed. Xerox PARC, San Francisco, CA.]] Kiczales, G., Ed. 1996. Proceedings of Reflection'96, G. Kiczales, ed. Xerox PARC, San Francisco, CA.]]"},{"key":"e_1_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Kiczales G. des Rivieres J. and Bobrow D. G. 1991. The Art of the Metaobject Protocol. MIT Press Cambridge MA.]] Kiczales G. des Rivieres J. and Bobrow D. G. 1991. The Art of the Metaobject Protocol. MIT Press Cambridge MA.]]","DOI":"10.7551\/mitpress\/1405.001.0001"},{"volume-title":"Proceedings of the First Annual Symposium on Logic in Computer Science. IEEE Computer Society Press","author":"Knoblock T. B.","key":"e_1_2_1_46_1","unstructured":"Knoblock , T. B. and Constable , R. L . 1986. Formalized metareasoning in type theory . In Proceedings of the First Annual Symposium on Logic in Computer Science. IEEE Computer Society Press , Los Alamitos, CA., 237--248.]] Knoblock, T. B. and Constable, R. L. 1986. Formalized metareasoning in type theory. In Proceedings of the First Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA., 237--248.]]"},{"key":"e_1_2_1_47_1","volume-title":"Logic Colloquium '82","author":"Makowsky J. A.","year":"1984","unstructured":"Makowsky , J. A. 1984 . Model theoretic issues in theoretical computer science, part I: Relational data bases and abstract data types . In Logic Colloquium '82 ( Florence, Italy). North Holland, Amsterdam, The Netherlands, 303--343.]] Makowsky, J. A. 1984. Model theoretic issues in theoretical computer science, part I: Relational data bases and abstract data types. In Logic Colloquium '82 (Florence, Italy). North Holland, Amsterdam, The Netherlands, 303--343.]]"},{"key":"e_1_2_1_48_1","doi-asserted-by":"crossref","unstructured":"Mart\u00ed-Oliet N. and Meseguer J. 1994. General logics and logical frameworks. In What is a Logical System? D. Gabbay Ed. Oxford University Press Oxford U.K. 355--392.]] Mart\u00ed-Oliet N. and Meseguer J. 1994. General logics and logical frameworks. In What is a Logical System? D. Gabbay Ed. Oxford University Press Oxford U.K. 355--392.]]","DOI":"10.1093\/oso\/9780198538592.003.0014"},{"key":"e_1_2_1_49_1","doi-asserted-by":"crossref","unstructured":"Mart\u00ed-Oliet N. and Meseguer J. 2002a. Rewriting logic as a logical and semantic framework. In Handbook of Philosophical Logic 2nd ed. D. Gabbay and F. Guenthner Eds. Kluwer Academic Publishers Amsterdam The Netherlands 1--87. First published as SRI Tech. Report SRI-CSL-93-05 August 1993.]] Mart\u00ed-Oliet N. and Meseguer J. 2002a. Rewriting logic as a logical and semantic framework. In Handbook of Philosophical Logic 2nd ed. D. Gabbay and F. Guenthner Eds. Kluwer Academic Publishers Amsterdam The Netherlands 1--87. First published as SRI Tech. Report SRI-CSL-93-05 August 1993.]]","DOI":"10.1007\/978-94-017-0464-9_1"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00357-7"},{"key":"e_1_2_1_51_1","unstructured":"Matthews S. 1992. Reflection in logical systems. See Smith and Yonezawa {1992} 178--183.]] Matthews S. 1992. Reflection in logical systems. See Smith and Yonezawa {1992} 178--183.]]"},{"key":"e_1_2_1_52_1","unstructured":"Matthews S. Smaill A. and Basin D. 1993. Experience with FS0 as a framework theory. In Logical Environments G. Huet and G. Plotkin Eds. Cambridge University Press Cambridge U.K. 61--82.]] Matthews S. Smaill A. and Basin D. 1993. Experience with FS0 as a framework theory. In Logical Environments G. Huet and G. Plotkin Eds. Cambridge University Press Cambridge U.K. 61--82.]]"},{"volume-title":"Twelfth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press","author":"McDowell R.","key":"e_1_2_1_53_1","unstructured":"McDowell , R. and Miller , D . 1997. A logic for reasoning with higher-order abstract syntax . In Twelfth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press , Los Alamitos, CA., 434--445.]] McDowell, R. and Miller, D. 1997. A logic for reasoning with higher-order abstract syntax. In Twelfth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA., 434--445.]]"},{"volume-title":"Logic Colloquium'87, H.-D. Ebbinghaus et al., Eds. North-Holland","author":"Meseguer J.","key":"e_1_2_1_54_1","unstructured":"Meseguer , J. 1989. General logics . In Logic Colloquium'87, H.-D. Ebbinghaus et al., Eds. North-Holland , Amsterdam, The Netherlands , 275--329.]] Meseguer, J. 1989. General logics. In Logic Colloquium'87, H.-D. Ebbinghaus et al., Eds. North-Holland, Amsterdam, The Netherlands, 275--329.]]"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_2_1_56_1","volume-title":"Proceedings of WADT'97","volume":"1376","author":"Meseguer J.","year":"1998","unstructured":"Meseguer , J. 1998 a. Membership algebra as a semantic framework for equational specification . In Proceedings of WADT'97 , F. Parisi-Presicce, Ed. Lecture Notes in Computer Science , vol. 1376 . Springer-Verlag, Berlin, Germany, 18--61.]] Meseguer, J. 1998a. Membership algebra as a semantic framework for equational specification. In Proceedings of WADT'97, F. Parisi-Presicce, Ed. Lecture Notes in Computer Science, vol. 1376. Springer-Verlag, Berlin, Germany, 18--61.]]"},{"key":"e_1_2_1_57_1","volume-title":"Computational Logic","author":"Meseguer J.","year":"1997","unstructured":"Meseguer , J. 1998b. Research directions in rewriting logic . In Computational Logic , NATO Advanced Study Institute, Marktoberdorf, Germany , July 29--August 6, 1997 , U. Berger and H. Schwichtenberg, Eds. Springer-Verlag , Berlin, Germany.]] Meseguer, J. 1998b. Research directions in rewriting logic. In Computational Logic, NATO Advanced Study Institute, Marktoberdorf, Germany, July 29--August 6, 1997, U. Berger and H. Schwichtenberg, Eds. Springer-Verlag, Berlin, Germany.]]"},{"key":"e_1_2_1_58_1","volume-title":"Proceedings of the Conference on Typed Lambda Calculi and Applications, M. Bezem and J.-F. Groote, Eds. Lecture Notes in Computer Science","volume":"664","author":"Paulin-Mohring C.","year":"1993","unstructured":"Paulin-Mohring , C. 1993 . Inductive definitions in the system Coq---rules and properties . In Proceedings of the Conference on Typed Lambda Calculi and Applications, M. Bezem and J.-F. Groote, Eds. Lecture Notes in Computer Science , vol. 664 . Springer-Verlag, Berlin, Germany. LIP Res. rep. 92--49.]] Paulin-Mohring, C. 1993. Inductive definitions in the system Coq---rules and properties. In Proceedings of the Conference on Typed Lambda Calculi and Applications, M. Bezem and J.-F. Groote, Eds. Lecture Notes in Computer Science, vol. 664. Springer-Verlag, Berlin, Germany. LIP Res. rep. 92--49.]]"},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the 12th International Conference on Automated Deduction (CADE-12)","volume":"814","author":"Paulson L. C.","year":"1994","unstructured":"Paulson , L. C. 1994 a. A fixedpoint approach to implementing (co)inductive definitions . In Proceedings of the 12th International Conference on Automated Deduction (CADE-12) (Nancy, France). Lecture Notes in Artificial Intelligence , vol. 814 . Springer-Verlag, Berlin, Germany.]] Paulson, L. C. 1994a. A fixedpoint approach to implementing (co)inductive definitions. In Proceedings of the 12th International Conference on Automated Deduction (CADE-12) (Nancy, France). Lecture Notes in Artificial Intelligence, vol. 814. Springer-Verlag, Berlin, Germany.]]"},{"volume-title":"A Generic Theorem Prover","author":"Paulson L. C.","key":"e_1_2_1_60_1","unstructured":"Paulson , L. C. 1994b. Isabelle : A Generic Theorem Prover ; with Contributions by Tobias Nipkow. Lecture Notes in Computer Science, vol. 828 . Springer , Berlin, Germany.]] Paulson, L. C. 1994b. Isabelle : A Generic Theorem Prover; with Contributions by Tobias Nipkow. Lecture Notes in Computer Science, vol. 828. Springer, Berlin, Germany.]]"},{"key":"e_1_2_1_61_1","series-title":"Lecture Notes in Computer Science","volume-title":"1992. Proceedings of the Third Workshop on Meta-programming in Logic","author":"Pettorossi A.","unstructured":"Pettorossi , A. , Ed. 1992. Proceedings of the Third Workshop on Meta-programming in Logic . Lecture Notes in Computer Science , vol. 649 . Springer-Verlag, Berlin , Germany .]] Pettorossi, A., Ed. 1992. Proceedings of the Third Workshop on Meta-programming in Logic. Lecture Notes in Computer Science, vol. 649. Springer-Verlag, Berlin, Germany.]]"},{"key":"e_1_2_1_62_1","volume-title":"Proceedings of the 16th International Conference on Automated Deduction (CADE-16)","volume":"1632","author":"Pfenning F.","unstructured":"Pfenning , F. and Sch\u00fcrmann , C . 1999. System description: Twelf---a meta-logical framework for deductive systems . In Proceedings of the 16th International Conference on Automated Deduction (CADE-16) , H. Ganzinger, Ed. Lecture Notes in Artificial Intelligence , vol. 1632 . Springer-Verlag, Berlin, Germany, 202--206.]] Pfenning, F. and Sch\u00fcrmann, C. 1999. System description: Twelf---a meta-logical framework for deductive systems. In Proceedings of the 16th International Conference on Automated Deduction (CADE-16), H. Ganzinger, Ed. Lecture Notes in Artificial Intelligence, vol. 1632. Springer-Verlag, Berlin, Germany, 202--206.]]"},{"key":"e_1_2_1_64_1","volume-title":"Proceedings for the Third International Conference on Typed Lambda Calculus and Applications (TLCA'97)","author":"Ruess H.","year":"1997","unstructured":"Ruess , H. 1997 . Computational reflection in the calculus of constructions and its application to theorem proving . In Proceedings for the Third International Conference on Typed Lambda Calculus and Applications (TLCA'97) (Nancy, France), R. Hindley, Ed. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 319--335.]] Ruess, H. 1997. Computational reflection in the calculus of constructions and its application to theorem proving. In Proceedings for the Third International Conference on Typed Lambda Calculus and Applications (TLCA'97) (Nancy, France), R. Hindley, Ed. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 319--335.]]"},{"key":"e_1_2_1_66_1","volume-title":"Proceedings of Logic for Programming, Artificial Intelligence, and Reasoning (LPAR","volume":"2250","author":"Sch\u00fcrmann C.","year":"2001","unstructured":"Sch\u00fcrmann , C. 2001 . A type-theoretic approach to induction with higher-order encodings . In Proceedings of Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001). Lecture Notes in Computer Science , vol. 2250 . Springer-Verlag, Berlin, Germany, 266--281.]] Sch\u00fcrmann, C. 2001. A type-theoretic approach to induction with higher-order encodings. In Proceedings of Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001). Lecture Notes in Computer Science, vol. 2250. Springer-Verlag, Berlin, Germany, 266--281.]]"},{"key":"e_1_2_1_67_1","volume-title":"Proceedings of the 15th International Conference on Automated Deduction (CADE-15)","volume":"1421","author":"Sch\u00fcrmann C.","unstructured":"Sch\u00fcrmann , C. and Pfenning , F . 1998. Automated theorem proving in a simple meta-logic for LF . In Proceedings of the 15th International Conference on Automated Deduction (CADE-15) (Lindau, Germany), C. Kirchner and H. Kirchner, Eds. Lecture Notes in Computer Science , vol. 1421 . Springer-Verlag, Berlin, Germany, 286--300.]] Sch\u00fcrmann, C. and Pfenning, F. 1998. Automated theorem proving in a simple meta-logic for LF. In Proceedings of the 15th International Conference on Automated Deduction (CADE-15) (Lindau, Germany), C. Kirchner and H. Kirchner, Eds. Lecture Notes in Computer Science, vol. 1421. Springer-Verlag, Berlin, Germany, 286--300.]]"},{"key":"e_1_2_1_68_1","volume-title":"Proceedings of the Tarski Symposium, L. Henkin, Ed. American Mathematical Society","author":"Scott D.","year":"1974","unstructured":"Scott , D. 1974 . Completeness and axiomatizability in many-valued logic . In Proceedings of the Tarski Symposium, L. Henkin, Ed. American Mathematical Society , Providence, RI, 411--435.]] Scott, D. 1974. Completeness and axiomatizability in many-valued logic. In Proceedings of the Tarski Symposium, L. Henkin, Ed. American Mathematical Society, Providence, RI, 411--435.]]"},{"volume-title":"Cambridge University Press","author":"Shankar N.","key":"e_1_2_1_69_1","unstructured":"Shankar , N. 1994. Metamathematics , Machines, and G\u00f6del's Proof . Cambridge University Press , Cambridge , U.K. ]] Shankar, N. 1994. Metamathematics, Machines, and G\u00f6del's Proof. Cambridge University Press, Cambridge, U.K.]]"},{"volume-title":"Proc. IMSA'92---International Workshop on Reflection and Meta-Level Architecture. Information-Technology Promotion Agency","author":"Smith B.","key":"e_1_2_1_70_1","unstructured":"Smith , B. and Yonezawa , A. , Eds . 1992 . Proc. IMSA'92---International Workshop on Reflection and Meta-Level Architecture. Information-Technology Promotion Agency , Tokyo, Japan.]] Smith, B. and Yonezawa, A., Eds. 1992. Proc. IMSA'92---International Workshop on Reflection and Meta-Level Architecture. Information-Technology Promotion Agency, Tokyo, Japan.]]"},{"key":"e_1_2_1_71_1","volume-title":"Proceedings of POPL'84","author":"Smith B. C.","year":"1984","unstructured":"Smith , B. C. 1984 . Reflection and semantics in Lisp . In Proceedings of POPL'84 . ACM Press, New York, NY, 23--35.]] 10.1145\/800017.800513 Smith, B. C. 1984. Reflection and semantics in Lisp. In Proceedings of POPL'84. ACM Press, New York, NY, 23--35.]] 10.1145\/800017.800513"},{"volume-title":"Handbook of Mathematical Logic","author":"Smorynski C.","key":"e_1_2_1_72_1","unstructured":"Smorynski , C. 1977. The incompleteness theorems . In Handbook of Mathematical Logic , J. Barwise, Ed. North-Holland, Amsterdam , The Netherlands , 821--865.]] Smorynski, C. 1977. The incompleteness theorems. In Handbook of Mathematical Logic, J. Barwise, Ed. North-Holland, Amsterdam, The Netherlands, 821--865.]]"},{"volume-title":"Oxford University Press","author":"Smullyan R. M.","key":"e_1_2_1_73_1","unstructured":"Smullyan , R. M. 1994. Diagonalization and Self-Reference. Oxford University Press , Oxford , U.K. ]] Smullyan, R. M. 1994. Diagonalization and Self-Reference. Oxford University Press, Oxford, U.K.]]"},{"key":"e_1_2_1_74_1","volume-title":"Tech. Rep. AIM-453. MIT AI-Lab","author":"Steele Jr., G. L.","year":"1978","unstructured":"Steele , Jr., G. L. and Sussman , G. J . 1978 . The art of the interpreter or, the modularity complex. Tech. Rep. AIM-453. MIT AI-Lab , Cambridge , MA .]] Steele, Jr., G. L. and Sussman, G. J. 1978. The art of the interpreter or, the modularity complex. Tech. Rep. AIM-453. MIT AI-Lab, Cambridge, MA.]]"},{"key":"e_1_2_1_75_1","volume-title":"Third International Workshop on Rewriting Logic and its Applications, K. Futatsugi, Ed. Electronic Notes in Theoretical Computer Science","volume":"36","author":"Stehr M.-O.","year":"2000","unstructured":"Stehr , M.-O. 2000 . CINNI---a generic calculus of explicit substitutions and its application to \u03bb-, &sigmav;- and &pi;-calculi . In Third International Workshop on Rewriting Logic and its Applications, K. Futatsugi, Ed. Electronic Notes in Theoretical Computer Science , vol. 36 . Elsevier, Amsterdam, The Netherlands, 71--92.]] Stehr, M.-O. 2000. CINNI---a generic calculus of explicit substitutions and its application to \u03bb-, &sigmav;- and &pi;-calculi. In Third International Workshop on Rewriting Logic and its Applications, K. Futatsugi, Ed. Electronic Notes in Theoretical Computer Science, vol. 36. Elsevier, Amsterdam, The Netherlands, 71--92.]]"},{"volume-title":"Proceedings of LFM'99: Workshop on Logical Frameworks and Meta-languages","author":"Stehr M.-O.","key":"e_1_2_1_76_1","unstructured":"Stehr , M.-O. and Meseguer , J . 1999. Pure type systems in rewriting logic . In Proceedings of LFM'99: Workshop on Logical Frameworks and Meta-languages , Paris, France. Available online at http:\/\/www.cs.bell-labs.com\/&sim;felty\/LFM99\/.]] Stehr, M.-O. and Meseguer, J. 1999. Pure type systems in rewriting logic. In Proceedings of LFM'99: Workshop on Logical Frameworks and Meta-languages, Paris, France. Available online at http:\/\/www.cs.bell-labs.com\/&sim;felty\/LFM99\/.]]"},{"key":"e_1_2_1_77_1","unstructured":"Stehr M.-O. Naumov P. and Meseguer J. 2000. A proof-theoretic approach to the HOL-Nuprl connection with applications to proof translation. Manuscript SRI International Menlo Park CA. Available online at http:\/\/www.csl.sri.com\/ stehr\/fi_eng.html.]] Stehr M.-O. Naumov P. and Meseguer J. 2000. A proof-theoretic approach to the HOL-Nuprl connection with applications to proof translation. Manuscript SRI International Menlo Park CA. Available online at http:\/\/www.csl.sri.com\/ stehr\/fi_eng.html.]]"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/5956.5957"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/321978.321991"},{"key":"e_1_2_1_80_1","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/BF01806174","article-title":"The mystery of the tower revealed","volume":"1","author":"Wand M.","year":"1988","unstructured":"Wand , M. and Friedman , D. P. 1988 . The mystery of the tower revealed . Lisp Symbol. Computat. 1 , 1, 11 -- 38 .]] Wand, M. and Friedman, D. P. 1988. The mystery of the tower revealed. Lisp Symbol. Computat. 1, 1, 11--38.]]","journal-title":"Lisp Symbol. Computat."},{"key":"e_1_2_1_81_1","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":"Weyhrauch R. W.","year":"1980","unstructured":"Weyhrauch , R. W. 1980 . Prolegomena to a theory of mechanized formal reasoning . Art. Intell. 13 , 133 -- 170 .]] Weyhrauch, R. W. 1980. Prolegomena to a theory of mechanized formal reasoning. Art. Intell. 13, 133--170.]]","journal-title":"Art. Intell."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1013560.1013566","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1013560.1013566","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:19:03Z","timestamp":1750263543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1013560.1013566"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,7]]},"references-count":76,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2004,7]]}},"alternative-id":["10.1145\/1013560.1013566"],"URL":"https:\/\/doi.org\/10.1145\/1013560.1013566","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2004,7]]},"assertion":[{"value":"2004-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}