{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:04Z","timestamp":1749125164966,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540417392"},{"type":"electronic","value":"9783540447160"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44716-4_23","type":"book-chapter","created":{"date-parts":[[2007,8,15]],"date-time":"2007-08-15T18:16:34Z","timestamp":1187201794000},"page":"359-374","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["A simply typed context calculus with first-class environments"],"prefix":"10.1007","author":[{"given":"Masahiko","family":"Sato","sequence":"first","affiliation":[]},{"given":"Takafumi","family":"Sakurai","sequence":"additional","affiliation":[]},{"given":"Yukiyoshi","family":"Kameyama","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,21]]},"reference":[{"key":"23_CR1","unstructured":"Barendregt, H. P., The Lambda Calculus, Its Syntax and Semantics, North-Holland, 1981."},{"key":"23_CR2","unstructured":"Bloo, R. and Rose, K.H., Preservation of Strong Normalization in Named Lambda Calculi with Explicit Substitution and Garbage Collection, Proceedings of CSN\u201995 (Computer Science in Netherlands), van Vliet J.C. (ed.), 1995. (ftp:\/\/ftp.diku.dk\/diku\/semantics\/papers\/D-246.ps)"},{"key":"23_CR3","unstructured":"Bognar, M. and de Vrijer, R., A calculus of lambda calculus contexts, available at: http:\/\/www.cs.vu.nl\/~mirna\/new.ps.gz."},{"key":"23_CR4","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"D. G. de Bruijn","year":"1972","unstructured":"de Bruijn, D. G., Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem, Indag. Math. 34, pp. 381\u2013392, 1972.","journal-title":"Indag. Math."},{"issue":"2","key":"23_CR5","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/S0304-3975(97)00150-3","volume":"192","author":"Laurent Dami","year":"1998","unstructured":"Dami, L., A Lambda-Calculus for Dynamic Binding, pp. 201\u2013231, Theoretical Computer Science 192, 1998.","journal-title":"Theoretical Computer Science"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Fiore, M., Plotkin, G., and Turi, D., Abstract Syntax and Variable Binding (Extended Abstract), Proc. 14th Symposium on Logic in Computer Science, pp. 193\u2013202, 1999.","DOI":"10.1109\/LICS.1999.782615"},{"key":"23_CR7","unstructured":"Hashimoto, M. and Ohori, A., A typed context calculus, Preprint RIMS-1098, Res. Inst. for Math. Sci., Kyoto Univ., 1996, Journal version is to appear in Theoretical Computer Science."},{"issue":"6","key":"23_CR8","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1145\/232629.232652","volume":"31","author":"Shinn-Der Lee","year":"1996","unstructured":"Lee, S.-R., and D. P. Friedman, Enriching the Lambda Calculus with Contexts: Toward a Theory of Incremental Program Construction, ACM SIGPLAN Notices, Proc. International Conference on Functional Programming, pp. 239\u2013250, 1996.","journal-title":"ACM SIGPLAN Notices"},{"key":"23_CR9","doi-asserted-by":"publisher","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 12, pp. 171\u2013201, 1999.","journal-title":"Higher-Order and Symbolic Computation"},{"key":"23_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0014062","volume-title":"Typed Lambda Calculi and Applications","author":"P.-A. Melli\u00e9s","year":"1995","unstructured":"Melli\u00e9s, P.-A., Typed \u03bb-calculi with explicit substitutions may not terminate, Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 902, pp. 328\u2013349, 1995."},{"key":"23_CR11","unstructured":"Pitts, A.M., Some notes on inductive and co-inductive techniques in the semantics of functional programs, Notes Series BRICS-NS-94-5, Department of Computer Science, University of Aarhus, 1994."},{"key":"23_CR12","series-title":"Master Thesis","volume-title":"An interpretation of a context calculus in an environment calculus","author":"H. Sakurada","year":"1999","unstructured":"Sakurada, H., An interpretation of a context calculus in an environment calculus, Master Thesis, Dept. of Information Science, Kyoto Univ., 1999 (in Japanese)."},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Sands, D., Computing with Contexts-a simple approach, Proc. Higher-Order Operational Techniques in Semantics, HOOTS II, 16 pages, Electronic Notes in Theoretical Computer Science 10, 1998.","DOI":"10.1016\/S1571-0661(05)80694-2"},{"key":"23_CR14","doi-asserted-by":"publisher","first-page":"455","DOI":"10.2977\/prims\/1195179055","volume":"21","author":"M. Sato","year":"1985","unstructured":"Sato, M., Theory of Symbolic Expressions, II, Publ. of Res. Inst. for Math. Sci., Kyoto Univ., 21, pp. 455\u2013540, 1985.","journal-title":"Publ. of Res. Inst. for Math. Sci."},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Sato, M., Sakurai T., and Burstall, R., Explicit Environments, Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 1581, pp. 340\u2013354, 1999.","DOI":"10.1007\/3-540-48959-2_24"},{"issue":"1","key":"23_CR16","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/0304-3975(93)90240-T","volume":"112","author":"Carolyn Talcott","year":"1993","unstructured":"Talcott, C., A Theory of binding structures and applications to rewriting, Theoretical Computer Science 112: 1, pp. 99\u2013143, 1993.","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44716-4_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T10:55:13Z","timestamp":1737370513000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44716-4_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540417392","9783540447160"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-44716-4_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"21 March 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}