{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:11:41Z","timestamp":1775790701457,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":49,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540666240","type":"print"},{"value":"9783540480921","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48092-7_6","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T17:01:46Z","timestamp":1186765306000},"page":"114-136","source":"Crossref","is-referenced-by-count":54,"title":["Type and Effect Systems"],"prefix":"10.1007","author":[{"given":"Flemming","family":"Nielson","sequence":"first","affiliation":[]},{"given":"Hanne Riis","family":"Nielson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,3,24]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"T. Amtoft, F. Nielson, and H. R. Nielson. Type and Effect Systems: Behaviours for Concurrency. Imperial College Press, 1999.","DOI":"10.1142\/p132"},{"issue":"3","key":"6_CR2","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1017\/S0956796897002700","volume":"7","author":"T. Amtoft","year":"1997","unstructured":"T. Amtoft, F. Nielson, and H.R. Nielson. Type and behaviour reconstruction for higher-order concurrent programs. Journal of Functional Programming, 7(3):321\u2013347, 1997.","journal-title":"Journal of Functional Programming"},{"key":"6_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-62503-8_9","volume-title":"Analysis and Verification of Multiple-Agent Languages","author":"T. Amtoft","year":"1997","unstructured":"T. Amtoft, F. Nielson, H.R. Nielson, and J. Ammann. Polymorphic subtyping for effect analysis: The dynamic semantics. In Analysis and Verification of Multiple-Agent Languages, volume 1192 of Lecture Notes in Computer Science, pages 172\u2013206. Springer, 1997."},{"key":"6_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BFb0023861","volume-title":"Proc. Second International Symposium on Logical Foundations of Computer Science","author":"P. N. Benton","year":"1992","unstructured":"P. N. Benton. Strictness logic and polymorphic invariance. In Proc. Second International Symposium on Logical Foundations of Computer Science, volume 620 of Lecture Notes in Computer Science, pages 33\u201344. Springer, 1992."},{"key":"6_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1007\/3-540-57264-3_42","volume-title":"Proc. WSA \u201893","author":"P. N. Benton","year":"1993","unstructured":"P. N. Benton. Strictness properties of lazy algebraic datatypes. In Proc. WSA \u201893, volume 724 of Lecture Notes in Computer Science, pages 206\u2013217. Springer, 1993."},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"L. Damas and R. Milner. Principal type-schemes for functional programs. In Proc. POPL \u201882, pages 207\u2013212. ACM Press, 1982.","DOI":"10.1145\/582153.582176"},{"key":"6_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1007\/3-540-60360-3_37","volume-title":"Proc. SAS \u201895","author":"K.-F. Fax\u00e9n","year":"1995","unstructured":"K.-F. Fax\u00e9n. Optimizing lazy functional programs using flow inference. In Proc. SAS \u201895, volume 983 of Lecture Notes in Computer Science, pages 136\u2013153. Springer, 1995."},{"key":"6_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/3-540-62503-8_12","volume-title":"Proc. Analysis and Verification of Multiple-Agent Languages","author":"K.-F. Fax\u00e9n","year":"1997","unstructured":"K.-F. Fax\u00e9n. Polyvariance, polymorphism, and flow analysis. In Proc. Analysis and Verification of Multiple-Agent Languages, volume 1192 of Lecture Notes in Computer Science, pages 260\u2013278. Springer, 1997."},{"key":"6_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/3-540-50940-2_35","volume-title":"Proc. TAPSOFT \u201889","author":"Y.-C. Fuh","year":"1989","unstructured":"Y.-C. Fuh and P. Mishra. Polymorphic subtype inference: Closing the theory-practice gap. In Proc. TAPSOFT \u201889, volume 352 of Lecture Notes in Computer Science, pages 167\u2013183. Springer, 1989."},{"key":"6_CR10","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/0304-3975(90)90144-7","volume":"73","author":"Y.-C. Fuh","year":"1990","unstructured":"Y.-C. Fuh and P. Mishra. Type inference with subtypes. Theoretical Computer Science, 73:155\u2013175, 1990.","journal-title":"Theoretical Computer Science"},{"key":"6_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/3-540-60360-3_40","volume-title":"Proc. SAS \u201895","author":"N. Heintze","year":"1995","unstructured":"N. Heintze. Control-flow analysis and type systems. In Proc. SAS \u201895, volume 983 of Lecture Notes in Computer Science, pages 189\u2013206. Springer, 1995."},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Nevin Heintze and Jon G. Riecke. The SLam calculus: Programming with Secrecy and Integrity. In Proc. POPL \u201898, pages 365\u2013377. ACM Press, 1998.","DOI":"10.1145\/268946.268976"},{"key":"6_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/3-540-57880-3_19","volume-title":"Proc. ESOP \u201894","author":"F. Henglein","year":"1994","unstructured":"F. Henglein and C. Mossin. Polymorphic binding-time analysis. In Proc. ESOP \u201894, volume 788 of Lecture Notes in Computer Science, pages 287\u2013301. Springer, 1994."},{"key":"6_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1007\/3540543961_17","volume-title":"Proc. FPCA \u201891","author":"T. P. Jensen","year":"1991","unstructured":"T. P. Jensen. Strictness analysis in logical form. In Proc. FPCA \u201891, volume 523 of Lecture Notes in Computer Science, pages 352\u2013366. Springer, 1991."},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"T. P. Jensen. Disjunctive strictness analysis. In Proc. LICS \u201892, pages 174\u2013185, 1992.","DOI":"10.1109\/LICS.1992.185531"},{"key":"6_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/3-540-55253-7_17","volume-title":"Proc. ESOP \u201892","author":"M. P. Jones","year":"1992","unstructured":"M. P. Jones. A theory of qualified types. In Proc. ESOP \u201892, volume 582 of Lecture Notes in Computer Science, pages 287\u2013306. Springer, 1992."},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"N. D. Jones and F. Nielson. Abstract Interpretation: a Semantics-Based Tool for Program Analysis. In Handbook of Logic in Computer Science volume 4. Oxford University Press, 1995.","DOI":"10.1093\/oso\/9780198537809.003.0005"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"P. Jouvelot. Semantic Parallelization: a practical exercise in abstract interpretation. In Proc. POPL \u201887, pages 39\u201348, 1987.","DOI":"10.1145\/41625.41629"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"P. Jouvelot and D. K. Gifford. Reasoning about continuations with control effects. In Proc. PLDI \u201889, ACM SIGPLAN Notices, pages 218\u2013226. ACM Press, 1989.","DOI":"10.1145\/73141.74837"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"P. Jouvelot and D. K. Gifford. Algebraic reconstruction of types and effects. In Proc. POPL \u201891, pages 303\u2013310. ACM Press, 1990.","DOI":"10.1145\/99583.99623"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"J. M. Lucassen and D. K. Gifford. Polymorphic effect analysis. In Proc. POPL \u201888, pages 47\u201357. ACM Press, 1988.","DOI":"10.1145\/73560.73564"},{"key":"6_CR22","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"R. Milner. A theory of type polymorphism in programming. Journal of Computer Systems, 17:348\u2013375, 1978.","journal-title":"Journal of Computer Systems"},{"issue":"3","key":"6_CR23","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1017\/S0956796800000113","volume":"1","author":"J. Mitchell","year":"1991","unstructured":"J. Mitchell. Type inference with simple subtypes. Journal of Functional Programming, 1(3):245\u2013285, 1991.","journal-title":"Journal of Functional Programming"},{"key":"6_CR24","unstructured":"F. Nielson. A formal type system for comparing partial evaluators. In D. Bj\u00f8rner, A. P. Ershov, and N. D. Jones, editors, Proc. Partial Evaluation and Mixed Computation, pages 349\u2013384. North Holland, 1988."},{"key":"6_CR25","series-title":"Lect Notes Comput Sci","first-page":"355","volume-title":"Proc. PARLE\u201889","author":"F. Nielson","year":"1989","unstructured":"F. Nielson. The typed \u03bb-calculus with firsrst-class processes. In Proc. PARLE\u201889, volume 366 of Lecture Notes in Computer Science, pages 355\u2013373. Springer, 1989."},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"F. Nielson and H. R. Nielson. Two-Level Functional Languages, volume 34 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.","DOI":"10.1017\/CBO9780511526572"},{"key":"6_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/3-540-57208-2_34","volume-title":"Proc. CONCUR\u201893","author":"F. Nielson","year":"1993","unstructured":"F. Nielson and H. R. Nielson. From CML to process algebras. In Proc. CONCUR\u201893, volume 715 of Lecture Notes in Computer Science, pages 493\u2013508. Springer, 1993."},{"key":"6_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/3-540-56596-5_43","volume-title":"Proc. REX\u201892 workshop on Semantics-foundations and applications","author":"F. Nielson","year":"1993","unstructured":"F. Nielson and H. R. Nielson. Layered predicates. In Proc. REX\u201892 workshop on Semantics-foundations and applications, volume 666 of Lecture Notes in Computer Science, pages 425\u2013456. Springer, 1993."},{"key":"6_CR29","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0304-3975(95)00017-8","volume":"155","author":"F. Nielson","year":"1996","unstructured":"F. Nielson and H. R. Nielson. From CML to its process algebra. Theoretical Computer Science, 155:179\u2013219, 1996.","journal-title":"Theoretical Computer Science"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"F. Nielson, H. R. Nielson, and C. L. Hankin. Principles of Program Analysis. Springer, 1999.","DOI":"10.1007\/978-3-662-03811-6"},{"key":"6_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/3-540-62503-8_10","volume-title":"Analysis and Verification of Multiple-Agent Languages","author":"F. Nielson","year":"1997","unstructured":"F. Nielson, H.R. Nielson, and T. Amtoft. Polymorphic subtyping for effect analysis: The algorithm. In Analysis and Verification of Multiple-Agent Languages, volume 1192 of Lecture Notes in Computer Science, pages 207\u2013243. Springer, 1997."},{"key":"6_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BFb0053595","volume-title":"Proc. FASE \u201898","author":"H. R. Nielson","year":"1998","unstructured":"H. R. Nielson, T. Amtoft, and F. Nielson. Behaviour analysis and safety conditions: a case study in CML. In Proc. FASE \u201898, number 1382 in Lecture Notes in Computer Science, pages 255\u2013269. Springer, 1998."},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"H. R. Nielson and F. Nielson. Higher-Order Concurrent Programs with Finite Communication Topology. In Proc. POPL \u201894. Springer, 1994.","DOI":"10.1145\/174675.174538"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"H. R. Nielson and F. Nielson. Communication analysis for Concurrent ML. In F. Nielson, editor, ML with Concurrency, Monographs in Computer Science, pages 185\u2013235. Springer, 1997.","DOI":"10.1007\/978-1-4612-2274-3_7"},{"key":"6_CR35","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-62503-8_8","volume-title":"Analysis and Verification of Multiple-Agent Languages","author":"H.R. Nielson","year":"1997","unstructured":"H.R. Nielson, F. Nielson, and T. Amtoft. Polymorphic subtyping for effect analysis: The static semantics. In Analysis and Verification of Multiple-Agent Languages, volume 1192 of Lecture Notes in Computer Science, pages 141\u2013171. Springer, 1997."},{"key":"6_CR36","series-title":"Technical Report FN-19","volume-title":"A structural approach to operational semantics","author":"G. D. Plotkin","year":"1981","unstructured":"G. D. Plotkin. A structural approach to operational semantics. Technical Report FN-19, DAIMI, Aarhus University, Denmark, 1981."},{"key":"6_CR37","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"671","DOI":"10.1007\/3-540-56610-4_97","volume-title":"Proc. TAP-SOFT \u201893","author":"G. S. Smith","year":"1993","unstructured":"G. S. Smith. Polymorphic inference with overloading and subtyping. In Proc. TAP-SOFT \u201893, volume 668 of Lecture Notes in Computer Science, pages 671\u2013685. Springer, 1993."},{"key":"6_CR38","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/0167-6423(94)00020-4","volume":"23","author":"G. S. Smith","year":"1994","unstructured":"G. S. Smith. Polymorphic type schemes for functional programs with overloading and subtyping. Science of Computer Programming, 23:197\u2013226, 1994.","journal-title":"Science of Computer Programming"},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"J.-P. Talpin and P. Jouvelot. The type and effect discipline. In Proc. LICS \u201892, pages 162\u2013173, 1992.","DOI":"10.1109\/LICS.1992.185530"},{"issue":"2","key":"6_CR40","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1006\/inco.1994.1046","volume":"111","author":"J.-P. Talpin","year":"1994","unstructured":"J.-P. Talpin and P. Jouvelot. The type and effect discipline. Information and Computation, 111(2):245\u2013296, 1994.","journal-title":"Information and Computation"},{"key":"6_CR41","unstructured":"Y.-M. Tang. Control-Flow Analysis by Effect Systems and Abstract Interpretation. PhD thesis, Ecole des Mines de Paris, 1994."},{"key":"6_CR42","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(90)90018-D","volume":"89","author":"M. Tofte","year":"1990","unstructured":"M. Tofte. Type inference for polymorphic references. Information and Computation, 89:1\u201334, 1990.","journal-title":"Information and Computation"},{"issue":"3","key":"6_CR43","first-page":"1","volume":"20","author":"M. T. Ofte","year":"1998","unstructured":"M. T ofte and L. Birkedal. A region inference algorithm. ACM TOPLAS, 20(3):1\u201344, 1998.","journal-title":"ACM TOPLAS"},{"key":"6_CR44","doi-asserted-by":"crossref","unstructured":"M. Tofte and J.-P. Talpin. Implementing the call-by-value lambda-calculus using a stack of regions. In Proc. POPL \u201894, pages 188\u2013201. ACM Press, 1994.","DOI":"10.1145\/174675.177855"},{"key":"6_CR45","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1006\/inco.1996.2613","volume":"132","author":"M. Tofte","year":"1997","unstructured":"M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132:109\u2013176, 1997.","journal-title":"Information and Computation"},{"key":"6_CR46","doi-asserted-by":"crossref","unstructured":"M. Wand. Specifying the correctness of binding-time analysis. In Proc. POPL \u201893, pages 137\u2013143, 1993.","DOI":"10.1145\/158511.158614"},{"key":"6_CR47","unstructured":"R. Wilhelm. Global flow analysis and optimization in the MUG2 compiler generating system. In S. S. Muchnick and N. D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 5. Prentice Hall International, 1981."},{"key":"6_CR48","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1007\/3-540-55253-7_28","volume-title":"Proc. ESOP \u201892","author":"A. K. Wright","year":"1992","unstructured":"A. K. Wright. Typing references by effect inference. In Proc. ESOP \u201892, volume 582 of Lecture Notes in Computer Science, pages 473\u2013491. Springer, 1992."},{"key":"6_CR49","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A. K. Wright","year":"1994","unstructured":"A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115:38\u201394, 1994.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Correct System Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48092-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,17]],"date-time":"2024-02-17T09:59:45Z","timestamp":1708163985000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48092-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540666240","9783540480921"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/3-540-48092-7_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}