{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T01:53:05Z","timestamp":1768701185891,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642022722","type":"print"},{"value":"9783642022739","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02273-9_25","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T14:12:17Z","timestamp":1246025537000},"page":"341-355","source":"Crossref","is-referenced-by-count":4,"title":["A Logical Foundation for Environment Classifiers"],"prefix":"10.1007","author":[{"given":"Takeshi","family":"Tsukada","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Atsushi","family":"Igarashi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","volume-title":"Partial Evaluation and Automatic Program Generation","author":"N.D. Jones","year":"1993","unstructured":"Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs (1993)"},{"issue":"1-3","key":"25_CR2","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1016\/j.scico.2004.03.011","volume":"52","author":"C. Consel","year":"2004","unstructured":"Consel, C., Lawall, J.L., Meur, A.F.L.: A tour of Tempo: A program specializer for the C language. Science of Computer Programming\u00a052(1-3), 341\u2013370 (2004)","journal-title":"Science of Computer Programming"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Wickline, P., Lee, P., Pfenning, F.: Run-time code generation and Modal-ML. In: Proc. of PLDI 1998, pp. 224\u2013235 (1998)","DOI":"10.21236\/ADA339112"},{"issue":"2","key":"25_CR4","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1145\/316686.316697","volume":"21","author":"M. Poletto","year":"1999","unstructured":"Poletto, M., Hsieh, W.C., Engler, D.R., Kaashoek, M.F.: \u2018C and tcc: A language and compiler for dynamic code generation. ACM TOPLAS\u00a021(2), 324\u2013369 (1999)","journal-title":"ACM TOPLAS"},{"key":"25_CR5","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/S0304-3975(00)00053-0","volume":"248","author":"W. Taha","year":"2000","unstructured":"Taha, W., Sheard, T.: MetaML and multi-stage programming with explicit annotations. Theoretical Computer Science\u00a0248, 211\u2013242 (2000)","journal-title":"Theoretical Computer Science"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/BFb0026825","volume-title":"Programming Languages: Implementations, Logics and Programs","author":"R. Gl\u00fcck","year":"1995","unstructured":"Gl\u00fcck, R., J\u00f8rgensen, J.: Efficient multi-level generating extensions for program specialization. In: Swierstra, S.D. (ed.) PLILP 1995. LNCS, vol.\u00a0982, pp. 259\u2013278. Springer, Heidelberg (1995)"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Davies, R.: A temporal-logic approach to binding-time analysis. In: Proc. of LICS 1996, pp. 184\u2013195 (1996)","DOI":"10.1109\/LICS.1996.561317"},{"issue":"3","key":"25_CR8","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/382780.382785","volume":"48","author":"R. Davies","year":"2001","unstructured":"Davies, R., Pfenning, F.: A modal analysis of staged computation. J. ACM\u00a048(3), 555\u2013604 (2001)","journal-title":"J. ACM"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Taha, W., Nielsen, M.F.: Environment classifiers. In: Proc. of POPL 2003, pp. 26\u201337 (2003)","DOI":"10.1145\/604131.604134"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Yuse, Y., Igarashi, A.: A modal type system for multi-level generating extensions with persistent code. In: Proc. of PPDP 2006, pp. 201\u2013212 (2006)","DOI":"10.1145\/1140335.1140360"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Kim, I.S., Yi, K., Calcagno, C.: A polymorphic modal type system for lisp-like multi-staged languages. In: Proc. of POPL 2006, pp. 257\u2013268 (2006)","DOI":"10.1145\/1111037.1111060"},{"key":"25_CR12","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1093\/oso\/9780198537618.003.0005","volume-title":"Handbook of Logic in Computer Science","author":"C. Stirling","year":"1992","unstructured":"Stirling, C.: Modal and temporal logics. In: Handbook of Logic in Computer Science, vol.\u00a02, pp. 477\u2013563. Oxford University Press, Oxford (1992)"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49099-X_13","volume-title":"Programming Languages and Systems","author":"E. Moggi","year":"1999","unstructured":"Moggi, E., Taha, W., Benaissa, Z.E.A., Sheard, T.: An idealized MetaML: Simpler, and more expressive. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"25_CR14","unstructured":"Benaissa, Z.E.A., Moggi, E., Taha, W., Sheard, T.: Logical modalities and multi-stage programming. In: Proc. of IMLA 1999 (1999)"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-540-24725-8_7","volume-title":"Programming Languages and Systems","author":"C. Calcagno","year":"2004","unstructured":"Calcagno, C., Moggi, E., Taha, W.: ML-like inference for classifiers. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 79\u201393. Springer, Heidelberg (2004)"},{"key":"25_CR16","unstructured":"Kojima, K., Igarashi, A.: On constructive linear-time temporal logic. In: Proc. of IMLA 2008 (2008)"},{"issue":"5","key":"25_CR17","doi-asserted-by":"publisher","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. Functional Programming\u00a015(5), 893\u2013939 (2005)","journal-title":"J. Functional Programming"},{"issue":"3","key":"25_CR18","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1017\/S0956796802004598","volume":"13","author":"C. Calcagno","year":"2003","unstructured":"Calcagno, C., Moggi, E., Sheard, T.: Closed types for a safe imperative MetaML. Journal of Functional Programming\u00a013(3), 545\u2013571 (2003)","journal-title":"Journal of Functional Programming"},{"issue":"4","key":"25_CR19","first-page":"1","volume":"2002","author":"M. Sato","year":"2002","unstructured":"Sato, M., Sakurai, T., Kameyama, Y.: A simply typed context calculus with first-class environments. J. Functional and Logic Programming\u00a02002(4), 1\u201341 (2002)","journal-title":"J. Functional and Logic Programming"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Transactions on Computational Logic 9(3) (2008)","DOI":"10.1145\/1352582.1352591"},{"key":"25_CR21","first-page":"99","volume-title":"Handbook of Philosophical Logic","author":"D. Harel","year":"2002","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. In: Gabbay, D., Guenther, F. (eds.) Handbook of Philosophical Logic, 2nd edn., vol.\u00a04, pp. 99\u2013218. Springer, Heidelberg (2002)","edition":"2"},{"key":"25_CR22","doi-asserted-by":"publisher","first-page":"821","DOI":"10.1016\/S1570-2464(07)80017-6","volume-title":"Handbook of Modal Logics","author":"C. Areces","year":"2007","unstructured":"Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logics, pp. 821\u2013868. Elsevier, Amsterdam (2007)"},{"key":"25_CR23","unstructured":"Reed, J., Pfenning, F.: Intuitionistic letcc via labelled deduction. In: Proc. of M4M 2007 (2007)"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02273-9_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,14]],"date-time":"2024-03-14T22:03:37Z","timestamp":1710453817000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02273-9_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642022722","9783642022739"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02273-9_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}