{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:15:03Z","timestamp":1774988103637,"version":"3.50.1"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2008,3,1]],"date-time":"2008-03-01T00:00:00Z","timestamp":1204329600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci. China"],"published-print":{"date-parts":[[2008,3]]},"DOI":"10.1007\/s11704-008-0011-1","type":"journal-article","created":{"date-parts":[[2008,3,27]],"date-time":"2008-03-27T10:44:08Z","timestamp":1206614648000},"page":"12-21","source":"Crossref","is-referenced-by-count":2,"title":["Calculi of meta-variables"],"prefix":"10.1007","volume":"2","author":[{"given":"Masahiko","family":"SATO","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Takafumi","family":"Sakurai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yukiyoshi","family":"Kameyama","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Atsushi","family":"Igarashi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2008,3,28]]},"reference":[{"key":"11_CR1","unstructured":"Kleene S C. Introduction to metamathematics. North-Holland, 1952"},{"key":"11_CR2","unstructured":"Shoenfield J R. Mathematical logic. Addison-Wesley, 1967"},{"issue":"1","key":"11_CR3","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper R, Honsell F, Plotkin G. A framework for defining logics. Journal of the Association for Computing Machinery, 1993, 40(1):143\u2013194","journal-title":"Journal of the Association for Computing Machinery"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Sato M. Theory of judgments and derivations. In: Discovery Science, LNAI 2281, 2001, 78\u2013122","DOI":"10.1007\/3-540-45884-0_5"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Sato M, Sakurai T, Kameyama Y, et al. Calculi of meta-variables. In: Proceedings of CSL 2003, LNCS 2803, 2003, 484\u2013497","DOI":"10.1007\/978-3-540-45220-1_39"},{"key":"11_CR6","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1023\/A:1010052222987","volume":"12","author":"I. Mason","year":"1999","unstructured":"Mason I. Computing with contexts. Higher-Order and Symbolic Computation, 1999, 12:171\u2013201","journal-title":"Higher-Order and Symbolic Computation"},{"issue":"1\u20132","key":"11_CR7","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/S0304-3975(00)00174-2","volume":"266","author":"M. Hashimoto","year":"2001","unstructured":"Hashimoto M, Ohori A. A typed context calculus. Theoretical Computer Science, 2001, 266(1\u20132):249\u2013272","journal-title":"Theoretical Computer Science"},{"key":"11_CR8","first-page":"1","volume":"4","author":"M. Sato","year":"2002","unstructured":"Sato M, Sakurai T, Kameyama Y. A simply typed context calculus with first-class environments. Journal of Functional and Logic Programming, 2002, 4:1\u201341","journal-title":"Journal of Functional and Logic Programming"},{"key":"11_CR9","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/S0747-7171(89)80045-8","volume":"7","author":"M. Takahashi","year":"1989","unstructured":"Takahashi M. Parallel reductions in l-calculus. Journal of Symbolic Computation, 1989, 7:113\u2013123","journal-title":"Journal of Symbolic Computation"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Geuvers H, Jojgov G. Open proofs and open terms: a basis for interactive logic. In: Proceedings of CSL 2002, LNCS 2471, 2002, 537\u2013552","DOI":"10.1007\/3-540-45793-3_36"},{"issue":"1","key":"11_CR11","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/0304-3975(93)90240-T","volume":"112","author":"C. Talcott","year":"1993","unstructured":"Talcott C. A theory of binding structures and applications to rewriting. Theoretical Computer Science, 1993, 112(1):99\u2013143","journal-title":"Theoretical Computer Science"},{"key":"11_CR12","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/S0304-3975(97)00150-3","volume":"192","author":"L. Dami","year":"1998","unstructured":"Dami L. A lambda-calculus for dynamic binding. Theoretical Computer Science, 1998, 192:201\u2013231","journal-title":"Theoretical Computer Science"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Sands D. Computing with contexts \u2014 a simple approach. Electronic Notes in Theoretical Computer Science, 10, 1998","DOI":"10.1016\/S1571-0661(05)80694-2"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Gl\u00fcck R, J\u00f8rgensen J. Efficient multi-level generating extensions for program specialization. In: Proceedings of Programming Languages, Implementations, Logics and Programs (PLILP\u201995), LNCS 982, 1995, 259\u2013278","DOI":"10.1007\/BFb0026825"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Davies R. A temporal-logic approach to binding-time analysis. In: 11th Annual IEEE Symposium on Logic in Computer Science (LICS\u201996), 1996, 184\u2013195","DOI":"10.1109\/LICS.1996.561317"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Yuse Y, Igarashi A. A modal type system for multi-level generating extensions with persistent code. In: Proceedings of PPDP, 2006, 201\u2013212","DOI":"10.1145\/1140335.1140360"},{"key":"11_CR17","unstructured":"Yamamoto K, Okamoto A, Sato M, et al. A typed lambda calculus with quasi-quotation (in Japanese). In: Informal Proceedings of the 4th JSSST Workshop on Programming and Programming Languages, 2003, 87\u2013102"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Nanevski A, Pfenning F, Pientka B. Contextual modal type theory. Transactions on Computational Logic, to appear","DOI":"10.1145\/1352582.1352591"},{"issue":"4","key":"11_CR19","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1017\/S0960129501003322","volume":"11","author":"F. Pfenning","year":"2001","unstructured":"Pfenning F, Davies R. A judgmental reconstruction of modal logic. Mathematical Structure in Computer Science, 2001, 11(4):511\u2013540","journal-title":"Mathematical Structure in Computer Science"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Gabbay MJ. A NEW calculus for contexts. In: Proceedings of 7th Int. ACM SIGPLAN Conf. on Principles and Practice of Declarative Programming, 2005, 94\u2013105","DOI":"10.1145\/1069774.1069783"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Hamana M. Free \u03a3-Monoids: a higher-order syntax with metavariables. In: Proceedings of APLAS, 2004, 348\u2013363","DOI":"10.1007\/978-3-540-30477-7_23"}],"container-title":["Frontiers of Computer Science in China"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-008-0011-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-008-0011-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-008-0011-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T21:00:45Z","timestamp":1559422845000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-008-0011-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,3]]}},"alternative-id":["11"],"URL":"https:\/\/doi.org\/10.1007\/s11704-008-0011-1","relation":{},"ISSN":["1673-7350","1673-7466"],"issn-type":[{"value":"1673-7350","type":"print"},{"value":"1673-7466","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,3]]}}}