{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T15:24:54Z","timestamp":1725809094835},"publisher-location":"Cham","reference-count":10,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319116280"},{"type":"electronic","value":"9783319116297"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-319-11629-7_3","type":"book-chapter","created":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T10:24:01Z","timestamp":1415960641000},"page":"19-25","source":"Crossref","is-referenced-by-count":0,"title":["Incorporating First-Order Unification into Functional Language via First-Class Environments"],"prefix":"10.1007","author":[{"given":"Shin-ya","family":"Nishizaki","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"3_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit substitutions. Journal of Functional Programming\u00a01(4), 375\u2013416 (1991)","journal-title":"Journal of Functional Programming"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Baarer, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1999)","DOI":"10.1017\/CBO9781139172752"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, J., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 447\u2013533. Elsevier Science Publishers (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"3_CR4","unstructured":"Barendregt, H.P.: The Lambda Calculus. Elsevier (1984)"},{"key":"3_CR5","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1016\/0304-3975(91)90230-Y","volume":"82","author":"P.L. Curien","year":"1991","unstructured":"Curien, P.L.: An abstract framework for environment machines. Theor. Comput. Sci.\u00a082, 389\u2013402 (1991)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"3_CR6","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1145\/226643.226675","volume":"43","author":"P.L. Curien","year":"1996","unstructured":"Curien, P.L., Hardin, T., L\u00e9vy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions. J. ACM\u00a043(2), 363\u2013397 (1996)","journal-title":"J. ACM"},{"key":"3_CR7","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions, extended abstract. In: Proceedings of the Symposium on Logic in Computer Science, pp. 22\u201339. Springer (1987)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/BFb0039592","volume-title":"STACS 87","author":"G. Kahn","year":"1987","unstructured":"Kahn, G.: Natural Semantics. In: Brandenburg, F.J., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol.\u00a0247, pp. 22\u201339. Springer, Heidelberg (1987)"},{"issue":"6","key":"3_CR9","doi-asserted-by":"publisher","first-page":"1055","DOI":"10.2977\/prims\/1195164948","volume":"30","author":"S. Nishizaki","year":"1995","unstructured":"Nishizaki, S.: Simply typed lambda calculus with first-class environments. Publications of Reseach Institute for Mathematical Sciences Kyoto University\u00a030(6), 1055\u20131121 (1995)","journal-title":"Publications of Reseach Institute for Mathematical Sciences Kyoto University"},{"issue":"3","key":"3_CR10","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1023\/A:1010010314528","volume":"13","author":"S. Nishizaki","year":"2000","unstructured":"Nishizaki, S.: Polymorphic environment calculus and its type inference algorithm. Higher-Order and Symbolic Computation\u00a013(3), 239\u2013278 (2000)","journal-title":"Higher-Order and Symbolic Computation"}],"container-title":["Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering","Signal Processing and Information Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11629-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,26]],"date-time":"2020-08-26T19:27:54Z","timestamp":1598470074000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11629-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319116280","9783319116297"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11629-7_3","relation":{},"ISSN":["1867-8211","1867-822X"],"issn-type":[{"type":"print","value":"1867-8211"},{"type":"electronic","value":"1867-822X"}],"subject":[],"published":{"date-parts":[[2014]]}}}