{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T14:10:01Z","timestamp":1751983801376,"version":"3.41.2"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2000,9,1]],"date-time":"2000-09-01T00:00:00Z","timestamp":967766400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,9,1]],"date-time":"2000-09-01T00:00:00Z","timestamp":967766400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order and Symbolic Computation"],"published-print":{"date-parts":[[2000,9]]},"DOI":"10.1023\/a:1010010314528","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T00:56:42Z","timestamp":1040605002000},"page":"239-278","source":"Crossref","is-referenced-by-count":19,"title":["A Polymorphic Environment Calculus and its Type-Inference Algorithm"],"prefix":"10.1007","volume":"13","author":[{"given":"Shin-Ya","family":"Nishizaki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"272061_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., and L\u00e9vy, J.-J. Explicit substitutions. Journal of Functional Programming\n1(4) (1991) 375\u2013416.","journal-title":"Journal of Functional Programming"},{"key":"272061_CR2","unstructured":"Barendregt, H.P. The Lambda Calculus. Elsevier, 1984."},{"issue":"3","key":"272061_CR3","first-page":"1","volume":"4","author":"W. Clinger","year":"1991","unstructured":"Clinger, W. and Rees, J. Revised4 report on the algorithmic language Scheme. ACMLisp Pointers\n4(3) (1991) 1\u201355.","journal-title":"ACMLisp Pointers"},{"key":"272061_CR4","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1016\/S0019-9958(86)80047-X","volume":"69","author":"P.-L. Curien","year":"1986","unstructured":"Curien, P.-L. Categorical combinators. Information and Control\n69 (1986) 188\u2013254.","journal-title":"Information and Control"},{"key":"272061_CR5","doi-asserted-by":"crossref","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. Theoretical Computer Science\n82 (1991) 389\u2013402.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"272061_CR6","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1145\/226643.226675","volume":"43","author":"P.-L. Curien","year":"1996","unstructured":"Curien, P.-L., Hardin, T., and L\u00e9vy, J.-J. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM\n43(2) (1996) 362-397.","journal-title":"Journal of the ACM"},{"key":"272061_CR7","doi-asserted-by":"crossref","unstructured":"Dowek, G., Hardin, T., and Kirchner, C. Higher-order unification via explicit substitutions, extended abstract. In Proceedings of the Symposium on Logic in Computer Science, 1995, pp. 366\u2013374.","DOI":"10.1109\/LICS.1995.523271"},{"issue":"3","key":"272061_CR8","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1016\/0304-3975(87)90109-5","volume":"52","author":"M. Felleisen","year":"1987","unstructured":"Felleisen, M., Friedman, D.P., Kohlbecker, E., and Duba, B. A syntactic theory of sequential control. Theoretical Computer Science\n52(3) (1987) 205\u2013237.","journal-title":"Theoretical Computer Science"},{"key":"272061_CR9","unstructured":"Gallesio, E. STk Reference Manual Version 3.99. 1998."},{"key":"272061_CR10","doi-asserted-by":"crossref","unstructured":"Gelernter, D., Jagannathan, S., and London, T. Environments as first-class objects. In Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, 1987, pp. 98\u2013110.","DOI":"10.1145\/41625.41634"},{"key":"272061_CR11","volume-title":"Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieur","author":"J.-Y. Girard","year":"1972","unstructured":"Girard, J.-Y. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieur. Th\u00e8se d' \u00c9tat, Universit\u00e9 de Paris VII, Paris, France, 1972."},{"key":"272061_CR12","unstructured":"Girard, J.-Y., Taylor, P., and Lafont, Y. Cambridge Tracts in Computer Science, Vol. 7: Proofs and Types. Cambridge University Press, 1989."},{"key":"272061_CR13","unstructured":"Hanson, C. MIT Scheme Reference Manual, 1.62 ed. MIT, 1996."},{"key":"272061_CR14","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(89)90105-9","volume":"65","author":"T. Hardin","year":"1989","unstructured":"Hardin, T. Confluence results for the pure strong categorical logic ccl, \u03bb-calculi as subsystems of ccl. Theoretical Computer Science\n65 (1989) 291\u2013342.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"272061_CR15","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1145\/177492.177578","volume":"16","author":"S. Jagannathan","year":"1994","unstructured":"Jagannathan, S. Metalevel building blocks for modular systems.ACMTransaction of Programming Languages and Systems\n16(3) (1994) 456\u2013492.","journal-title":"ACMTransaction of Programming Languages and Systems"},{"key":"272061_CR16","doi-asserted-by":"crossref","first-page":"127","DOI":"10.3233\/FI-1993-191-206","volume":"19","author":"L.A. Jategaonkar","year":"1993","unstructured":"Jategaonkar, L.A. and Mitchell, J.C. Type inference with extended pattern matching and subtypes. Fundamenta Informaticae\n19 (1993) 127\u2013166.","journal-title":"Fundamenta Informaticae"},{"key":"272061_CR17","doi-asserted-by":"crossref","unstructured":"Jouvelot, P. and Gifford, D.K. Algebraic reconstruction of types and effects. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, 1991, pp. 303\u2013310.","DOI":"10.1145\/99583.99623"},{"key":"272061_CR18","unstructured":"Kelsey, R., Clinger, W., and Rees, J. (Eds.). Revised5 report on the algorithmic language Scheme. Higher-Order and Symbolic Computation\n11(1) (1998) 7\u2013105. Also appears in ACM SIGPLAN Notices 33(9), September dy1998."},{"key":"272061_CR19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1093\/logcom\/2.1.1","volume":"2","author":"J.W. Klop","year":"1992","unstructured":"Klop, J.W. Term rewriting systems. In Handbook of Logic in Computer Science, Vol. 2. Clarendon Press, 1992, pp. 1\u2013116.","journal-title":"Handbook of Logic in Computer Science"},{"key":"272061_CR20","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1016\/0890-5401(88)90011-9","volume":"76","author":"B. Lampson","year":"1988","unstructured":"Lampson, B. and Burstall, R. Pebble, a kernel language for modules and abstract data types. Information and Computation\n76 (1988) 278-346.","journal-title":"Information and Computation"},{"key":"272061_CR21","unstructured":"Laumann, O. Elk\u2014The Extension Language Kit Scheme Reference. 1995."},{"issue":"2","key":"272061_CR22","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/BF01813016","volume":"4","author":"J.S. Miller","year":"1991","unstructured":"Miller, J.S. and Rozas, G.J. Free variables and first-class environments. Lisp and Symbolic Computation\n4(2) (1991) 107\u2013141.","journal-title":"Lisp and Symbolic Computation"},{"key":"272061_CR23","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/BFb0032396","volume":"792","author":"S. Nishizaki","year":"1994","unstructured":"Nishizaki, S. ML with first-class environments and its type inference algorithm. In Lecture Notes in Computer Science, Vol. 792: Logic, Language and Computation. Springer, 1994, pp. 95\u2013116.","journal-title":"Lecture Notes in Computer Science"},{"issue":"6","key":"272061_CR24","doi-asserted-by":"crossref","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. Publication of Research Institute for Mathematical Sciences Kyoto University\n30(6) (1995) 1055\u20131121.","journal-title":"Publication of Research Institute for Mathematical Sciences Kyoto University"},{"key":"272061_CR25","unstructured":"Nishizaki, S. Type inference for simply-typed environment calculus with shadowing. In Proceedings of the Fuji International Workshop on Functional and Logic Programming, 1995."},{"key":"272061_CR26","unstructured":"Nishizaki, S. and Akama, Y. Translations of first-class environments to records. In 1st International Workshop on Explicit Substitutions, 1998."},{"key":"272061_CR27","doi-asserted-by":"crossref","unstructured":"Ohori, A. A compilation method for ML-style polymorphic record calculi. In Conference Record of the Nineteenth Annual ACM Symposium on Principles of Programming Languages, 1992, pp. 154\u2013165.","DOI":"10.1145\/143165.143200"},{"key":"272061_CR28","doi-asserted-by":"crossref","unstructured":"Queinnec, C. and De Roure, D. Sharing code through first-class environments. In Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, 1996, pp. 251\u2013261.","DOI":"10.1145\/232627.232653"},{"key":"272061_CR29","unstructured":"R\u00e9my, D. Typechecking records and variants in a natural extention of ML. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989, pp. 60\u201367."},{"key":"272061_CR30","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications","author":"M. Sato","year":"1999","unstructured":"Sato, M., Sakurai, T., and Burstall, R. Explicit environments. In Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications, Jean-Yves Girard (Ed.). Springer-Verlag, L'Aquila, Italy, 1999. Lecture Notes in Computer Science 1581."},{"issue":"3","key":"272061_CR31","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1016\/0167-6423(96)00012-3","volume":"27","author":"J. Seaman","year":"1996","unstructured":"Seaman, J. and Iyer, S.P. An operational semantics of sharing in lazy evaluation. Science of Computer Programming\n27(3) (1996) 286\u2013322.","journal-title":"Science of Computer Programming"},{"key":"272061_CR32","unstructured":"Talcott, C. Reasoning about functions with effects. In Higher-Order Operational Techniques in Semantics, A.D. Gordon and A.M. Pitts, (Eds). Cambridge University Press, 1996, pp. 347\u2013390."},{"issue":"3","key":"272061_CR33","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1017\/S0956796800000393","volume":"2","author":"J.-P. Talpin","year":"1992","unstructured":"Talpin, J.-P. and Jouvelot, P. Polymorphic type, region and effect inference. Journal of Functional Programming\n2(3) (1992) 245\u2013271.","journal-title":"Journal of Functional Programming"},{"issue":"1","key":"272061_CR34","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(90)90018-D","volume":"89","author":"M. Tofte","year":"1990","unstructured":"Tofte, M. Type inference for polymorphic references. Information and Computation\n89(1) (1990) 1\u201334.","journal-title":"Information and Computation"},{"key":"272061_CR35","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(91)90050-C","volume":"93","author":"M. Wand","year":"1991","unstructured":"Wand, M. Type inference for record concatenation and multiple inheritance. Information and Computation\n93 (1991) 1\u201315.","journal-title":"Information and Computation"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1010010314528.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1010010314528\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1010010314528.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T13:56:07Z","timestamp":1751982967000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1010010314528"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,9]]},"references-count":35,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2000,9]]}},"alternative-id":["272061"],"URL":"https:\/\/doi.org\/10.1023\/a:1010010314528","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"type":"print","value":"1388-3690"},{"type":"electronic","value":"1573-0557"}],"subject":[],"published":{"date-parts":[[2000,9]]}}}