{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T22:00:45Z","timestamp":1747173645429,"version":"3.40.5"},"reference-count":121,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T00:00:00Z","timestamp":1551052800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Processing programs as data is one of the successes of functional and logic programming. Higher-order functions, as program-processing programs are called in functional programming, and meta-programs, as they are called in logic programming, are widespread declarative programming techniques. In logic programming, there is a gap between the meta-programming practice and its theory: The formalizations of meta-programming do not explicitly address its impredicativity and are not fully adequate. This article aims at overcoming this unsatisfactory situation by discussing the relevance of impredicativity to meta-programming, by revisiting former formalizations of meta-programming, and by defining Reflective Predicate Logic, a conservative extension of first-order logic, which provides a simple formalization of meta-programming.<\/jats:p>","DOI":"10.1017\/s1471068419000024","type":"journal-article","created":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T13:30:21Z","timestamp":1551101421000},"page":"99-146","source":"Crossref","is-referenced-by-count":2,"title":["In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming"],"prefix":"10.1017","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0532-6005","authenticated-orcid":false,"given":"FRAN\u00c7OIS","family":"BRY","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2019,2,25]]},"reference":[{"key":"S1471068419000024_ref117","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56282-6_6"},{"key":"S1471068419000024_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/355592.365646"},{"key":"S1471068419000024_ref29","doi-asserted-by":"publisher","DOI":"10.2307\/1968337"},{"key":"S1471068419000024_ref79","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-83189-8"},{"key":"S1471068419000024_ref54","doi-asserted-by":"publisher","DOI":"10.1007\/BF01700692"},{"volume-title":"Types and Programming Languages","year":"2002","author":"Pierce","key":"S1471068419000024_ref95"},{"volume-title":"Programming in Prolog","year":"1981","author":"Clocksin","key":"S1471068419000024_ref33"},{"key":"S1471068419000024_ref3","doi-asserted-by":"publisher","DOI":"10.3233\/FI-1996-281202"},{"key":"S1471068419000024_ref58","volume-title":"Term Indexing","volume":"1053","author":"Graf","year":"1996"},{"key":"S1471068419000024_ref5","first-page":"125","volume-title":"Proc. of the International Conference on Information Processing","author":"Backus","year":"1959"},{"volume-title":"Begriffsschrift \u2013 Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens","year":"1879","author":"Frege","key":"S1471068419000024_ref42"},{"key":"S1471068419000024_ref106","first-page":"1957","volume-title":"Automation of Reasoning","volume":"1","author":"Siekmann","year":"1983"},{"key":"S1471068419000024_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_15"},{"key":"S1471068419000024_ref52","first-page":"1","article-title":"Combining negation as failure and embedded implications in logic programs","volume":"19","author":"Giordano","year":"1994","journal-title":"Journal of Logic Programming"},{"key":"S1471068419000024_ref86","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"S1471068419000024_ref50","first-page":"68","volume-title":"The Collected Works of Gerhard Gentzen","author":"Gentzen","year":"1969"},{"key":"S1471068419000024_ref10","first-page":"288","volume-title":"Logic Programming \u2013 The 1995 International Symposium","author":"Barklund","year":"1995"},{"key":"S1471068419000024_ref6","first-page":"117","volume-title":"Handbook of Logic in Computer Science","volume":"2","author":"Barendregt","year":"1993"},{"key":"S1471068419000024_ref85","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326"},{"key":"S1471068419000024_ref94","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48660-7_14"},{"key":"S1471068419000024_ref12","doi-asserted-by":"crossref","first-page":"743","DOI":"10.1093\/logcom\/10.6.743","article-title":"Reflection principles in computational logic","volume":"10","author":"Barklund","year":"2000","journal-title":"Journal of Logic and Computation"},{"key":"S1471068419000024_ref99","first-page":"135","volume-title":"Machine Intelligence 4","author":"Robinson","year":"1969"},{"key":"S1471068419000024_ref81","unstructured":"McCarthy, J. and Levin, M. I. 1965. Lisp 1.5 Programmer\u2019s Manual. Tech. Rep., Computation Center, Massachusetts Institute of Technology, USA."},{"key":"S1471068419000024_ref24","doi-asserted-by":"crossref","unstructured":"Cervesato, I. and Rossi, G. 1992. Logic meta-programming facilities in \u2018LOG. Research Showcase @ CMU 6-1992, Carnegie Mellon University, School of Computer Science, Computer Science Department.","DOI":"10.1007\/3-540-56282-6_10"},{"volume-title":"Grundgesetze der Arithmetik, Band II","year":"1903","author":"Frege","key":"S1471068419000024_ref44"},{"key":"S1471068419000024_ref111","first-page":"261","article-title":"Der Wahrheitsbegriff in den formalisierten Sprachen","volume":"146","author":"Tarski","year":"1935","journal-title":"Studia Philosophica: commentarii Societatis Philosophicae Polonorum"},{"key":"S1471068419000024_ref32","first-page":"338","volume-title":"Polish Logic: 1920\u20131939","author":"Chwistek","year":"1967"},{"volume-title":"Symbolic Logic and Mechanical Theorem Proving","year":"1997","author":"Chang","key":"S1471068419000024_ref25"},{"key":"S1471068419000024_ref71","unstructured":"Kowalski, R. 1973. Predicate logic as a programming language. Memo 70, Department of Artificial Intelligence, Edinburgh University. Also in: Proc. IFIP Congress, Stockholm, North Holland, 1974, 569\u2013574."},{"key":"S1471068419000024_ref21","doi-asserted-by":"crossref","DOI":"10.1515\/9780691187068","volume-title":"Fixing Frege","author":"Burgess","year":"2005"},{"key":"S1471068419000024_ref2","doi-asserted-by":"publisher","DOI":"10.1109\/PROC.1986.13633"},{"key":"S1471068419000024_ref64","first-page":"23","volume-title":"Meta-Programming in Logic Programming, Workshop on Meta-Programming in Logic (META-88)","author":"Hill","year":"1988"},{"key":"S1471068419000024_ref82","doi-asserted-by":"publisher","DOI":"10.21236\/ADA065502"},{"key":"S1471068419000024_ref68","first-page":"387","volume-title":"Proc. International Conference on Logic Programming","author":"Jiang","year":"1994"},{"key":"S1471068419000024_ref53","unstructured":"G\u00f6del, K. 1930. \u00dcber die Vollst\u00e4ndigkeit des Logikkalk\u00fcls. Doctoral thesis, University of Vienna, Austria. In German, English translation: G\u00f6del (2002)."},{"key":"S1471068419000024_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-1641-1_1"},{"key":"S1471068419000024_ref75","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2877"},{"key":"S1471068419000024_ref57","first-page":"1929","volume-title":"On Formally Undecidable Propositions of Principia Mathematica and Related Systems I","volume":"I","author":"G\u00f6del","year":"1986"},{"volume-title":"From Frege to G\u00f6del: A Sourcebook in Mathematical Logic, 1879-1931","year":"1967, 2002","author":"Frege","key":"S1471068419000024_ref46"},{"key":"S1471068419000024_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037077"},{"key":"S1471068419000024_ref30","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S1471068419000024_ref7","first-page":"383","volume-title":"Meta-Programming in Logic Programming","author":"Barklund","year":"1989"},{"key":"S1471068419000024_ref18","first-page":"153","volume-title":"Logic Programming","author":"Bowen","year":"1982"},{"key":"S1471068419000024_ref31","first-page":"164","article-title":"Antynomje logikiformalnej","volume":"24","author":"Chwistek","year":"1921","journal-title":"Przeglad Filozoficzny"},{"key":"S1471068419000024_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2499937.2499942"},{"key":"S1471068419000024_ref119","first-page":"289","volume-title":"Logic Programming: Proceedings of the 1991 International Symposium","author":"Wadge","year":"1991"},{"key":"S1471068419000024_ref60","first-page":"480","volume-title":"Proc. 9th International Joint Conference on Artificial Intelligence (IJCAI)","volume":"1","author":"Halpern","year":"1985"},{"key":"S1471068419000024_ref110","first-page":"19","volume-title":"Proc. of the 2nd Workshop on Meta-Programming in Logic Programming (META)","author":"Sugano","year":"1990"},{"key":"S1471068419000024_ref93","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569807.008"},{"key":"S1471068419000024_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(93)90039-J"},{"key":"S1471068419000024_ref89","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1145\/377924.594925","article-title":"Preliminary report: International algebraic language","volume":"1","author":"Perlis","year":"1958","journal-title":"Communications of the ACM"},{"key":"S1471068419000024_ref61","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"S1471068419000024_ref112","first-page":"152","volume-title":"Logic, Semantics, Metamathematics, Papers from 1923 to 1938","author":"Tarski","year":"1935"},{"key":"S1471068419000024_ref87","unstructured":"Moschovakis, J. 1999, 2015. Intuitionistic Logic. The Metaphysics Research Lab, Center for the Study of Language and Information, Stanford University, Stanford, CA 94305-4115. https:\/\/plato.stanford.edu\/entries\/logic-intuitionistic\/."},{"year":"1976","author":"Huet","key":"S1471068419000024_ref67"},{"key":"S1471068419000024_ref65","first-page":"29","volume-title":"Transactions of the American Mathematical Society 146","author":"Hindley","year":"1969"},{"key":"S1471068419000024_ref55","first-page":"123","volume-title":"The Philosophy of Bertrand Russell","author":"G\u00f6del","year":"1944"},{"key":"S1471068419000024_ref23","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1145\/6041.6042","article-title":"On understanding types, data abstraction, and polymorphism","volume":"17","author":"Cardelli","year":"1985","journal-title":"ACM Computing Surveys"},{"key":"S1471068419000024_ref69","unstructured":"Kalsbeek, M. B. 1993. The Vanilla Metainterpreter for Definite Logic Programs and Ambivalent Syntax. Tech. Rep. CT 93-01, Institute for Logic Language and Computation, University of Amsterdam."},{"key":"S1471068419000024_ref76","doi-asserted-by":"crossref","DOI":"10.1515\/9783110199680","volume-title":"One Hundred Years of Russell\u2019s Paradox: Mathematics, Logic, Philosophy","author":"Link","year":"2004"},{"volume-title":"Proc. of the Fifth International Conference on Artificial Intelligence and Information-Control Systems of Robots \u2013 89","year":"1989","author":"Rossi","key":"S1471068419000024_ref100"},{"volume-title":"The G\u00f6del Programming Language","year":"1994","author":"Hill","key":"S1471068419000024_ref63"},{"key":"S1471068419000024_ref22","first-page":"2208","volume-title":"CRC Handbook of Computer Science and Engineering","author":"Cardelli","year":"2004"},{"key":"S1471068419000024_ref84","first-page":"810","volume-title":"Proc. Fifth International Conference and Symposium on Logic Programming","author":"Miller","year":"1988"},{"key":"S1471068419000024_ref38","first-page":"207","volume-title":"Proc. of the 9th Symposium on Principles of Programming Languages (POPL)","author":"Damas","year":"1982"},{"key":"S1471068419000024_ref1","first-page":"739","volume-title":"An introduction to inductive definitions. In Handbook of Mathematical Logic","author":"Aczel","year":"1977"},{"key":"S1471068419000024_ref113","unstructured":"Trump, D. 2017. \u201cWhy would Kim Jong-un insult me by calling me \u2018old\u2019, when I would NEVER call him \u2018short and fat\u2019? Oh well, I try so hard to be his friend \u2013 And maybe someday that will happen!\u201d. Twitter Web Client https:\/\/twitter.com\/realdonaldtrump\/status\/929511061954297857."},{"key":"S1471068419000024_ref78","doi-asserted-by":"publisher","DOI":"10.1007\/BF01079206"},{"key":"S1471068419000024_ref101","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/36.3.217"},{"key":"S1471068419000024_ref14","first-page":"395","volume-title":"Proc. of the 16th International Conference on Logic Programming (ICLP)","author":"Bezem","year":"1999"},{"volume-title":"Grundgesetze der Arithmetik, Band I","year":"1893","author":"Frege","key":"S1471068419000024_ref43"},{"key":"S1471068419000024_ref97","unstructured":"Robinson, A. and Voronkov, A. , Eds. 2001. Handbook of Automated Reasoning. Vol. 1. ScienceDirect."},{"key":"S1471068419000024_ref36","doi-asserted-by":"publisher","DOI":"10.1080\/09528139408953789"},{"key":"S1471068419000024_ref121","volume":"1\u20133","author":"Whitehead","year":"1910, 1912, 1913","journal-title":"Principia Mathematica"},{"key":"S1471068419000024_ref115","doi-asserted-by":"publisher","DOI":"10.1145\/321978.321991"},{"key":"S1471068419000024_ref90","first-page":"307","article-title":"Languages with self-reference i: Foundations","volume":"3","author":"Perlis","year":"1985","journal-title":"Artificial Intelligence"},{"key":"S1471068419000024_ref41","doi-asserted-by":"publisher","DOI":"10.1093\/0195148770.003.0019"},{"key":"S1471068419000024_ref40","unstructured":"Eshghi, K. 1986. Meta-language in Logic Programming. Ph.D. thesis, Department of Computing, Imperial College of Science and Technnology, University of London, UK."},{"key":"S1471068419000024_ref34","first-page":"254","volume-title":"Computational Logic: Logic Programming and Beyond (Festschrift in honour of Robert Kowalski)","volume":"2408","author":"Costantini","year":"2002"},{"key":"S1471068419000024_ref83","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(89)90031-9"},{"key":"S1471068419000024_ref17","doi-asserted-by":"crossref","DOI":"10.5962\/bhl.title.29413","volume-title":"An Investigation of the Laws of Thought on Which are Founded the Mathematical Theories of Logic and Probabilities","author":"Boole","year":"1854"},{"key":"S1471068419000024_ref35","first-page":"218","volume-title":"Proc. of the International Conference on Logic Programming","author":"Costantini","year":"1989"},{"key":"S1471068419000024_ref74","first-page":"354","volume-title":"Proc. of the 10th International Conference on Logic Programming","author":"Levi","year":"1993"},{"key":"S1471068419000024_ref118","doi-asserted-by":"publisher","DOI":"10.1515\/9783110853933"},{"key":"S1471068419000024_ref27","first-page":"24","volume-title":"Proc. IEEE Symposium on Logic Programming","author":"Chen","year":"1987"},{"key":"S1471068419000024_ref96","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1112\/plms\/s2-25.1.338","article-title":"The foundations of mathematics","volume":"225","author":"Ramsey","year":"1926","journal-title":"Proceedings of the London Mathematical Society, Series"},{"volume-title":"The Craft of Prolog","year":"1990","author":"O\u2019Keefe","key":"S1471068419000024_ref88"},{"volume-title":"Knowledge and Belief \u2013 An Introduction to the Logic of the Two Notions","year":"1964","author":"Hintikka","key":"S1471068419000024_ref66"},{"key":"S1471068419000024_ref51","first-page":"125","article-title":"Structured Prolog: A language for structured logic programming","volume":"15","author":"Giordano","year":"1994","journal-title":"Software-Concepts and Tools"},{"key":"S1471068419000024_ref122","first-page":"192","author":"De Schreye","year":"1992","journal-title":"Meta-Programming in Logic, Proc. of the 3rd International Workshop on Meta-Programming (META)"},{"key":"S1471068419000024_ref116","first-page":"1","volume-title":"Logic-based Knowledge Representation","author":"van Harmelen","year":"1989"},{"key":"S1471068419000024_ref104","first-page":"1909","volume-title":"The Collected Papers of Bertrand Russell","volume":"6","author":"Russell","year":"1986"},{"key":"S1471068419000024_ref9","first-page":"554","volume-title":"Logic Programming, Proceedings of the 1994 International Symposium","author":"Barklund","year":"1994"},{"key":"S1471068419000024_ref49","first-page":"288","article-title":"Investigations into logical deduction","volume":"1","author":"Gentzen","year":"1964","journal-title":"American Philosophical Quarterly"},{"key":"S1471068419000024_ref103","doi-asserted-by":"publisher","DOI":"10.2307\/2369948"},{"key":"S1471068419000024_ref47","first-page":"1070","volume-title":"Proc. of the Fifth International Conference on Logic Programming (ICLP)","author":"Gelfond","year":"1988"},{"volume-title":"Handbook of Epistemic Logic","year":"2015","author":"van Ditmarsch","key":"S1471068419000024_ref114"},{"volume-title":"The Art of Prolog","year":"1994","author":"Sterling","key":"S1471068419000024_ref108"},{"key":"S1471068419000024_ref59","first-page":"41","volume-title":"Logic Programming \u2013 International Conference on Logic Programming (ICLP)","author":"Haemmerl\u00e9","year":"2006"},{"key":"S1471068419000024_ref77","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1145\/942572.807045","article-title":"Programming with abstract data types","volume":"9","author":"Liskov","year":"1974","journal-title":"ACM SIGPLAN Notices"},{"key":"S1471068419000024_ref45","doi-asserted-by":"crossref","DOI":"10.1525\/9780520312364","volume-title":"The Basic Laws of Arithmetic","author":"Frege","year":"1964"},{"key":"S1471068419000024_ref102","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1112\/plms\/s2-4.1.29","article-title":"On some difficulties in the theory of transfinite numbers and order types","volume":"s2\u20134","author":"Russell","year":"1907","journal-title":"Proceedings of the London Mathematical Society"},{"key":"S1471068419000024_ref11","first-page":"830","volume-title":"Logic Programming, Proceedings of the Twelfth International Conference on Logic Programming","author":"Barklund","year":"1995"},{"key":"S1471068419000024_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/362929.362947"},{"key":"S1471068419000024_ref120","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(80)90015-6"},{"key":"S1471068419000024_ref98","unstructured":"Robinson, G. and Wos, L. 1968. Completeness of paramodulation. In Proc. of the Spring 1968 Meeting of the Association for Symbolic Logic, Journal of Symbolic Logic, Vol. 34, (1969), 102\u2013103."},{"key":"S1471068419000024_ref109","unstructured":"Sugano, H. 1989. Reflective Computation in Logic Language and Its Semantics. Tech. Rep., International Institute for Advanced Study of Social and Information Science, Fujitsu Limited."},{"volume-title":"Let\u2019s Talk Lisp","year":"1976","author":"Sikl\u00f3ssy","key":"S1471068419000024_ref107"},{"key":"S1471068419000024_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"S1471068419000024_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/322326.322339"},{"key":"S1471068419000024_ref92","first-page":"37","volume-title":"Meta-level Architectures and Reflection","author":"Perlis","year":"1988"},{"key":"S1471068419000024_ref20","first-page":"669","volume-title":"Proc. of the IEEE Symposium on Logic Programming","author":"Bowen","year":"1985"},{"key":"S1471068419000024_ref80","first-page":"317","volume-title":"ESOP\u201988: 2nd European Symposium on Programming","volume":"300","author":"Martelli","year":"1988"},{"key":"S1471068419000024_ref37","unstructured":"Damas, L. 1985. Type Assignment in Programming Languages. Ph.D. thesis, Report No. CST-33-85, University of Edinburgh."},{"key":"S1471068419000024_ref56","first-page":"582","volume-title":"From Frege to G\u00f6del: A Sourcebook in Mathematical Logic, 1879-1931","author":"G\u00f6del","year":"1967"},{"key":"S1471068419000024_ref73","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-450010-5.50019-0"},{"key":"S1471068419000024_ref8","first-page":"205","article-title":"Metaprogramming in logic","volume":"33","author":"Barklund","year":"1995","journal-title":"Encyclopedia of Computer Science and Technology"},{"key":"S1471068419000024_ref62","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/6.3.363"},{"key":"S1471068419000024_ref91","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(88)90038-0"},{"volume-title":"Logic For Problem Solving","year":"1979","author":"Kowalski","key":"S1471068419000024_ref72"},{"key":"S1471068419000024_ref70","first-page":"27","volume-title":"Meta-Logics and Logic Programming","author":"Kalsbeek","year":"1995"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068419000024","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,12]],"date-time":"2022-09-12T15:13:58Z","timestamp":1662995638000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068419000024\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,25]]},"references-count":121,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["S1471068419000024"],"URL":"https:\/\/doi.org\/10.1017\/s1471068419000024","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2019,2,25]]}}}