{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T03:25:33Z","timestamp":1781839533750,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642288685","type":"print"},{"value":"9783642288692","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28869-2_18","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:44:36Z","timestamp":1332449076000},"page":"357-376","source":"Crossref","is-referenced-by-count":11,"title":["Reasoning about Multi-stage Programs"],"prefix":"10.1007","author":[{"given":"Jun","family":"Inoue","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Walid","family":"Taha","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"18_CR1","first-page":"65","volume-title":"The Lazy Lambda Calculus","author":"S. Abramsky","year":"1990","unstructured":"Abramsky, S.: The Lazy Lambda Calculus, pp. 65\u2013116. Addison-Wesley, Boston (1990)"},{"key":"18_CR2","unstructured":"Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and The Foundations of Mathematics. North-Holland (1984)"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-17511-4_5","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Berger","year":"2010","unstructured":"Berger, M., Tratt, L.: Program Logics for Homogeneous Meta-programming. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 64\u201381. Springer, Heidelberg (2010)"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Brady, E., Hammond, K.: A verified staged interpreter is a verified compiler. In: 5th International Conference on Generative Programming and Component Engineering, pp. 111\u2013120. ACM (2006)","DOI":"10.1145\/1173706.1173724"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/11561347_18","volume-title":"Generative Programming and Component Engineering","author":"J. Carette","year":"2005","unstructured":"Carette, J., Kiselyov, O.: Multi-stage Programming with Functors and Monads: Eliminating Abstraction Overhead from Generic Code. In: Gl\u00fcck, R., Lowry, M. (eds.) GPCE 2005. LNCS, vol.\u00a03676, pp. 256\u2013274. Springer, Heidelberg (2005)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-540-76637-7_15","volume-title":"Programming Languages and Systems","author":"J. Carette","year":"2007","unstructured":"Carette, J., Kiselyov, O., Shan, C.-C.: Finally Tagless, Partially Evaluated: Tagless Staged Interpreters for Simpler Typed Languages. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol.\u00a04807, pp. 222\u2013238. Springer, Heidelberg (2007)"},{"key":"18_CR7","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1145\/1926385.1926397","volume-title":"38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"W. Choi","year":"2011","unstructured":"Choi, W., Aktemur, B., Yi, K., Tatsuta, M.: Static analysis of multi-staged programs via unstaging translation. In: 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 81\u201392. ACM, New York (2011)"},{"issue":"1","key":"18_CR8","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.scico.2005.10.013","volume":"62","author":"A. Cohen","year":"2006","unstructured":"Cohen, A., Donadio, S., Garzaran, M.J., Herrmann, C., Kiselyov, O., Padua, D.: In search of a program generator to implement generic transformations for high-performance computing. Sci. Comput. Program.\u00a062(1), 25\u201346 (2006)","journal-title":"Sci. Comput. Program."},{"key":"18_CR9","unstructured":"Dybvig, R.K.: Writing hygienic macros in scheme with syntax-case. Tech. Rep. TR356, Indiana University Computer Science Department (1992)"},{"issue":"1-2","key":"18_CR10","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0304-3975(98)00353-3","volume":"228","author":"A.D. Gordon","year":"1999","unstructured":"Gordon, A.D.: Bisimilarity as a theory of functional programming. Theoretical Computer Science\u00a0228(1-2), 5\u201347 (1999)","journal-title":"Theoretical Computer Science"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-15769-1_4","volume-title":"Static Analysis","author":"M. Heizmann","year":"2010","unstructured":"Heizmann, M., Jones, N., Podelski, A.: Size-Change Termination and Transition Invariants. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 22\u201350. Springer, Heidelberg (2010)"},{"issue":"1","key":"18_CR12","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.scico.2006.02.002","volume":"62","author":"C.A. Herrmann","year":"2006","unstructured":"Herrmann, C.A., Langhammer, T.: Combining partial evaluation and staged interpretation in the implementation of domain-specific languages. Sci. Comput. Program.\u00a062(1), 47\u201365 (2006)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"18_CR13","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1006\/inco.1996.0008","volume":"124","author":"D.J. Howe","year":"1996","unstructured":"Howe, D.J.: Proving congruence of bisimulation in functional programming languages. Inf. Comput.\u00a0124(2), 103\u2013112 (1996)","journal-title":"Inf. Comput."},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Inoue, J., Taha, W.: Reasoning about multi-stage programs. Tech. rep., Rice University Computer Science Department (October 2011)","DOI":"10.1007\/978-3-642-28869-2_18"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-73228-0_14","volume-title":"Typed Lambda Calculi and Applications","author":"B. Intrigila","year":"2007","unstructured":"Intrigila, B., Statman, R.: The Omega Rule is ${\\bf{\\Pi}^{1}_{1}}$ -Complete in the \u03bb\u03b2-Calculus. In: Ronchi Della Rocca, S. (ed.) TLCA 2007. LNCS, vol.\u00a04583, pp. 178\u2013193. Springer, Heidelberg (2007)"},{"key":"18_CR16","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1145\/1480945.1480962","volume-title":"2009 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation","author":"Y. Kameyama","year":"2009","unstructured":"Kameyama, Y., Kiselyov, O., Shan, C.-C.: Shifting the stage: Staging with delimited control. In: 2009 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pp. 111\u2013120. ACM, New York (2009)"},{"key":"18_CR17","first-page":"257","volume-title":"33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"I.S. Kim","year":"2006","unstructured":"Kim, I.S., Yi, K., Calcagno, C.: A polymorphic modal type system for LISP-like multi-staged languages. In: 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 257\u2013268. ACM, New York (2006)"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Kiselyov, O., Swadi, K.N., Taha, W.: A methodology for generating verified combinatorial circuits. In: Proc. of EMSOFT, pp. 249\u2013258. ACM (2004)","DOI":"10.1145\/1017753.1017794"},{"key":"18_CR19","first-page":"141","volume-title":"2006 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation","author":"V. Koutavas","year":"2006","unstructured":"Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: 2006 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, pp. 141\u2013152. ACM, New York (2006)"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Muller, R.: M-LISP: A representation-independent dialect of LISP with reduction semantics. ACM Trans. Program. Lang. Syst., 589\u2013616 (1992)","DOI":"10.1145\/133233.133254"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Plotkin, G.D.: The \u03bb-calculus is \u03c9-incomplete. J. Symb. Logic, 313\u2013317 (June 1974)","DOI":"10.2307\/2272645"},{"issue":"2","key":"18_CR22","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G.D. Plotkin","year":"1975","unstructured":"Plotkin, G.D.: Call-by-name, call-by-value and the \u03bb-calculus. Theor. Comput. Sci.\u00a01(2), 125\u2013159 (1975)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Rompf, T., Odersky, M.: Lightweight modular staging: A pragmatic approach to runtime code generation and compiled DSLs. In: 9th International Conference on Generative Programming and Component Engineering (2010)","DOI":"10.1145\/1868294.1868314"},{"key":"18_CR25","first-page":"275","volume-title":"Improvement Theory and its Applications","author":"D. Sands","year":"1998","unstructured":"Sands, D.: Improvement Theory and its Applications, pp. 275\u2013306. Cambridge University Press, New York (1998)"},{"key":"18_CR26","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1145\/1111542.1111570","volume-title":"2006 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation","author":"K. Swadi","year":"2006","unstructured":"Swadi, K., Taha, W., Kiselyov, O., Pa\u0161ali\u0107, E.: A monadic approach for avoiding code duplication when staging memoized functions. In: 2006 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, pp. 160\u2013169. ACM, New York (2006)"},{"key":"18_CR27","unstructured":"Taha, W.: Multistage Programming: Its Theory and Applications. Ph.D. thesis, Oregon Graduate Institute (1999)"},{"key":"18_CR28","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/604131.604134","volume-title":"30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"W. Taha","year":"2003","unstructured":"Taha, W., Nielsen, M.F.: Environment classifiers. In: 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 26\u201337. ACM, New York (2003)"},{"key":"18_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-642-02273-9_25","volume-title":"Typed Lambda Calculi and Applications","author":"T. Tsukada","year":"2009","unstructured":"Tsukada, T., Igarashi, A.: A Logical Foundation for Environment Classifiers. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol.\u00a05608, pp. 341\u2013355. Springer, Heidelberg (2009)"},{"key":"18_CR30","unstructured":"Westbrook, E., Ricken, M., Inoue, J., Yao, Y., Abdelatif, T., Taha, W.: Mint: Java multi-stage programming using weak separability. In: 2010 Conference on Programming Language Design and Implementation (2010)"},{"key":"18_CR31","doi-asserted-by":"crossref","unstructured":"Yang, Z.: Reasoning about code-generation in two-level languages. Tech. Rep. RS-00-46, BRICS (2000)","DOI":"10.7146\/brics.v7i46.20213"},{"key":"18_CR32","first-page":"201","volume-title":"8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming","author":"Y. Yuse","year":"2006","unstructured":"Yuse, Y., Igarashi, A.: A modal type system for multi-level generating extensions with persistent code. In: 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 201\u2013212. ACM, New York (2006)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28869-2_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T18:49:15Z","timestamp":1742755755000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28869-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288685","9783642288692"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28869-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}