{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T19:46:45Z","timestamp":1693856805254},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2008,1,4]],"date-time":"2008-01-04T00:00:00Z","timestamp":1199404800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2009,6]]},"DOI":"10.1007\/s10990-007-9022-0","type":"journal-article","created":{"date-parts":[[2008,1,3]],"date-time":"2008-01-03T20:52:41Z","timestamp":1199393561000},"page":"115-144","source":"Crossref","is-referenced-by-count":11,"title":["Directly reflective meta-programming"],"prefix":"10.1007","volume":"22","author":[{"given":"Aaron","family":"Stump","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2008,1,4]]},"reference":[{"key":"9022_CR1","volume-title":"The Java Programming Language","author":"K. Arnold","year":"2000","unstructured":"Arnold, K., Gosling, J., Holmes, D.: The Java Programming Language. Prentice-Hall, Englewood Cliffs (2000)"},{"key":"9022_CR2","doi-asserted-by":"crossref","unstructured":"Aydemir, B., Bohannon, A., Fairbairn, M., Foster, J., Pierce, B., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: The POPLmark challenge. In: Proceedings of the Eighteenth International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), 2005","DOI":"10.1007\/11541868_4"},{"issue":"6","key":"9022_CR3","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1017\/S0956796805005617","volume":"15","author":"C. Chen","year":"2005","unstructured":"Chen, C., Xi, H.: Meta-programming through typeful code representation. J.\u00a0Funct. Program. 15(6), 797\u2013835 (2005)","journal-title":"J.\u00a0Funct. Program."},{"key":"9022_CR4","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications","author":"M. Clavel","year":"1998","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J.: Metalevel computation in Maude. In: Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam (1998)"},{"key":"9022_CR5","series-title":"NATO ASI Series","volume-title":"Proof and Computation","author":"R. Constable","year":"1994","unstructured":"Constable, R.: Using reflection to explain and enhance type theory. In: Proof and Computation. NATO ASI Series. Springer, New York (1994)"},{"issue":"06","key":"9022_CR6","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1017\/S0956796801004282","volume":"12","author":"K. Crary","year":"2002","unstructured":"Crary, K., Weirich, S., Morrisett, G.: Intensional polymorphism in type-erasure semantics. J.\u00a0Funct. Program. 12(06), 567\u2013600 (2002)","journal-title":"J.\u00a0Funct. Program."},{"key":"9022_CR7","volume-title":"Combinatory Logic, vol.\u00a02","author":"H. Curry","year":"1972","unstructured":"Curry, H., Hindley, J., Seldin, J.: Combinatory Logic, vol.\u00a02. North-Holland, Amsterdam (1972)"},{"key":"9022_CR8","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0898-1221(79)90044-0","volume":"5","author":"M. Davis","year":"1979","unstructured":"Davis, M., Schwartz, J.: Metamathematical extensibility for theorem verifiers and proof-checkers. Comput. Math. Appl. 5, 217\u2013230 (1979)","journal-title":"Comput. Math. Appl."},{"key":"9022_CR9","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1145\/74877.74910","volume-title":"OOPSLA \u201989: Conference Proceedings on Object-Oriented Programming Systems, Languages and Applications","author":"J. Ferber","year":"1989","unstructured":"Ferber, J.: Computational reflection in class based object-oriented languages. In: OOPSLA \u201989: Conference Proceedings on Object-Oriented Programming Systems, Languages and Applications, pp. 317\u2013326. ACM Press, New York (1989)"},{"key":"9022_CR10","doi-asserted-by":"crossref","unstructured":"Ganz, S., Sabry, A., Taha, W.: Macros as multi-stage computations: Type-safe, generative, binding macros in MacroML. In: International Conference on Functional Programming, pp.\u00a074\u201385 (2001)","DOI":"10.1145\/507635.507646"},{"key":"9022_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/978-3-540-71289-3_9","volume-title":"Fundamental Approaches to Software Engineering, FASE 2007","author":"J. Gao","year":"2007","unstructured":"Gao, J., Heimdahl, M., Van Wyk, E.: Flexible and extensible notations for modeling languages. In: Fundamental Approaches to Software Engineering, FASE 2007. Lecture Notes in Computer Science, vol. 4422, pp. 102\u2013116. Springer, New York (2007)"},{"key":"9022_CR12","volume-title":"Proofs and Types","author":"J.-Y. Girard","year":"1990","unstructured":"Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge (1990)"},{"key":"9022_CR13","volume-title":"Smalltalk-80: The Language and Its Implementation","author":"A. Goldberg","year":"1983","unstructured":"Goldberg, A., Robson, D.: Smalltalk-80: The Language and Its Implementation. Addison-Wesley, Reading (1983)"},{"key":"9022_CR14","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A\u00a0survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995)"},{"key":"9022_CR15","doi-asserted-by":"crossref","unstructured":"Harrison, J.: The HOL Light System Reference (2006)","DOI":"10.1007\/11542384_3"},{"key":"9022_CR16","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Towards self-verification of HOL light. In: International Joint Conference on Automated Reasoning, 2006","DOI":"10.1007\/11814771_17"},{"key":"9022_CR17","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/11541868_11","volume-title":"18th International Conference on Theorem Proving in Higher Order Logics","author":"W. Hunt","year":"2005","unstructured":"Hunt, W., Kaufmann, M., Krug, R., Moore, J., Smith, E.: Meta reasoning in ACL2. In: Hurd, J., Melham, T. (eds.) 18th International Conference on Theorem Proving in Higher Order Logics, pp. 163\u2013178. Springer, New York (2005)"},{"key":"9022_CR18","unstructured":"Jefferson, S., Friedman, D.: A\u00a0simple reflective interpreter. In: IMSA\u201992 International Workshop on Reflection and Meta-Level Architecture, 1992"},{"key":"9022_CR19","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.: Computer-Aided Reasoning: An Approach. Kluwer Academic, Dordrecht (2000)"},{"issue":"9","key":"9022_CR20","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1145\/290229.290234","volume":"33","author":"R. Kelsey","year":"1998","unstructured":"Kelsey, R., Clinger, W., Rees, J., et al.: Revised5 report on the algorithmic language scheme. SIGPLAN Notices 33(9), 26\u201376 (1998)","journal-title":"SIGPLAN Notices"},{"key":"9022_CR21","doi-asserted-by":"crossref","unstructured":"Kim, I.-S., Yi, K., Calcagno, C.: A\u00a0polymorphic modal type system for lisp-like multi-staged languages. In: The 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.\u00a0257\u2013268 (2006)","DOI":"10.1145\/1111037.1111060"},{"key":"9022_CR22","volume-title":"Term Rewriting Systems","author":"J. Klop","year":"2003","unstructured":"Klop, J., de Vrijer, R.: Examples of TRSs and special rewriting formats. In: TERESE (ed.) Term Rewriting Systems. Cambridge University Press, Cambridge (2003). Chap.\u00a03"},{"key":"9022_CR23","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/319838.319859","volume-title":"LFP \u201986: Proceedings of the 1986 ACM Conference on LISP and Functional Programming","author":"E. Kohlbecker","year":"1986","unstructured":"Kohlbecker, E., Friedman, D., Felleisen, M., Duba, B.: Hygienic macro expansion. In: LFP \u201986: Proceedings of the 1986 ACM Conference on LISP and Functional Programming, pp. 151\u2013161. ACM Press, New York (1986)"},{"key":"9022_CR24","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Peyton Jones, S. (ed.) Proceedings of the 32nd ACM Symposium on Principles of Programming Languages, 2006","DOI":"10.1145\/1111037.1111042"},{"key":"9022_CR25","unstructured":"Leroy, X., Blazy, S., Dargaye, Z.: Formal verification of a C compiler front-end. In: Misra, J., Nipkow, T. (eds.) Proceedings of Formal Methods, 2006"},{"key":"9022_CR26","unstructured":"Lewis, B., LaLiberte, D., Stallman, R.: The GNU Manual Group: GNU Emacs Lisp Reference Manual. GNU Press (2000)"},{"issue":"4","key":"9022_CR27","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1145\/367177.367199","volume":"3","author":"J. McCarthy","year":"1960","unstructured":"McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine, Part\u00a0I. Commun. ACM 3(4), 184\u2013195 (1960)","journal-title":"Commun. ACM"},{"issue":"3","key":"9022_CR28","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1017\/S0956796800000423","volume":"2","author":"T. Mogensen","year":"1992","unstructured":"Mogensen, T.: Efficient self-interpretations in lambda calculus. J.\u00a0Funct. Program. 2(3), 345\u2013363 (1992)","journal-title":"J.\u00a0Funct. Program."},{"key":"9022_CR29","doi-asserted-by":"crossref","first-page":"727","DOI":"10.1007\/BFb0030637","volume-title":"International Joint Conference on Theory and Practice of Software Development (TAPSOFT\/FASE\u201997), vol.\u00a01214","author":"L. Moreau","year":"1997","unstructured":"Moreau, L.: A\u00a0syntactic theory of dynamic binding. In: International Joint Conference on Theory and Practice of Software Development (TAPSOFT\/FASE\u201997), vol.\u00a01214, pp. 727\u2013741. Springer, New York (1997)"},{"key":"9022_CR30","doi-asserted-by":"crossref","unstructured":"Nanevski, A.: Meta-programming with names and necessity. Technical Report CMU-CS-02-123R, Carnegie Mellon University (November 2002)","DOI":"10.1145\/581478.581498"},{"issue":"6","key":"9022_CR31","doi-asserted-by":"crossref","first-page":"893","DOI":"10.1017\/S095679680500568X","volume":"15","author":"A. Nanevski","year":"2005","unstructured":"Nanevski, A., Pfenning, F.: Staged computation with names and necessity. J.\u00a0Funct. Program. 15(6), 893\u2013939 (2005)","journal-title":"J.\u00a0Funct. Program."},{"key":"9022_CR32","volume-title":"The Implementation of Functional Programming Languages","author":"S. Peyton Jones","year":"1987","unstructured":"Peyton Jones, S.: The Implementation of Functional Programming Languages. Prentice-Hall, Englewood Cliffs (1987)"},{"key":"9022_CR33","volume-title":"Handbook of Automated Reasoning","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F.: Logical frameworks. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier and MIT Press, Cambridge (2001). Chap.\u00a021"},{"key":"9022_CR34","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: ACM SIGPLAN Symposium on Language Design and Implementation, 1988","DOI":"10.1145\/53990.54010"},{"key":"9022_CR35","volume-title":"Types and Programming Languages","author":"B. Pierce","year":"2002","unstructured":"Pierce, B.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"9022_CR36","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/3-540-62688-3_44","volume-title":"Proceedings of the Third International Conference on Typed Lambda Calculi and Applications","author":"H. Rue\u00df","year":"1997","unstructured":"Rue\u00df, H.: Computational reflection in the calculus of constructions and its application to theorem proving. In: Proceedings of the Third International Conference on Typed Lambda Calculi and Applications, pp. 319\u2013335. Springer, New York (1997)"},{"key":"9022_CR37","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/11417170_25","volume-title":"Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications","author":"C. Sch\u00fcrmann","year":"2005","unstructured":"Sch\u00fcrmann, C., Poswolsky, A., Sarnat, J.: The \u2207-calculus. Functional programming with higher-order encodings. In: Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications, pp. 339\u2013353. Springer, New York (2005)"},{"key":"9022_CR38","doi-asserted-by":"crossref","unstructured":"Siskind, J., Pearlmutter, B.: First-class nonstandard interpretations by opening closures. In: Proceedings of the Symposium on Principles of Programming Languages (POPL), 2007","DOI":"10.1145\/1190216.1190230"},{"key":"9022_CR39","doi-asserted-by":"crossref","unstructured":"Smith, B.: Reflection and semantics in LISP. In: Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp.\u00a023\u201335 (1984)","DOI":"10.1145\/800017.800513"},{"key":"9022_CR40","volume-title":"Common LISP: The Language","author":"G. Steele","year":"1990","unstructured":"Steele, G.: Common LISP: The Language, 2nd edn. Digital Press, Belford (1990)","edition":"2"},{"key":"9022_CR41","volume-title":"The C++ Programming Language","author":"B. Stroustrup","year":"1997","unstructured":"Stroustrup, B.: The C++ Programming Language, 3rd edn. Addison-Wesley, Reading (1997)","edition":"3"},{"key":"9022_CR42","unstructured":"Taha, W.: Multi-stage programming: Its theory and applications. Ph.D. thesis, Oregon Graduate Institute (November 1999)"},{"key":"9022_CR43","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual, Version V8.0 (2004). http:\/\/coq.inria.fr"},{"key":"9022_CR44","unstructured":"The GHC Team: The Glorious Glasgow Haskell Compilation System User\u2019s Guide, Version 6.6.1 (2007). http:\/\/www.haskell.org\/ghc\/docs\/latest\/html\/users_guide\/"},{"key":"9022_CR45","unstructured":"The PLT Group: PLT DrScheme: Programming Environment Manual (2007). http:\/\/download.plt-scheme.org\/doc\/drscheme\/"},{"key":"9022_CR46","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Theorems for free! In: 4th International Conference on Functional Programming and Computer Architecture, 1989","DOI":"10.1145\/99370.99404"},{"key":"9022_CR47","first-page":"215","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism","author":"C. Wadsworth","year":"1980","unstructured":"Wadsworth, C.: Some unusual \u03bb-calculus numeral systems. In: Seldin, J., Hindley, J. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp. 215\u2013230. Academic, New York (1980)"},{"issue":"3","key":"9022_CR48","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1023\/A:1007720632734","volume":"10","author":"M. Wand","year":"1998","unstructured":"Wand, M.: The theory of fexprs is trivial. Lisp Symb. Comput. 10(3), 189\u2013199 (1998)","journal-title":"Lisp Symb. Comput."},{"key":"9022_CR49","unstructured":"Westbrook, E.: Free variable types. In: Seventh Symposium on Trends in Functional Programming (TFP 06), April 2006"},{"issue":"1","key":"9022_CR50","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1145\/239912.239917","volume":"19","author":"A. Wright","year":"1997","unstructured":"Wright, A., Cartwright, R.: A\u00a0practical soft type system for scheme. ACM Trans. Program. Lang. Syst. 19(1), 87\u2013152 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9022-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-007-9022-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9022-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T00:29:08Z","timestamp":1630456148000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-007-9022-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1,4]]},"references-count":50,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,6]]}},"alternative-id":["9022"],"URL":"https:\/\/doi.org\/10.1007\/s10990-007-9022-0","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,1,4]]}}}