{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:15:28Z","timestamp":1770286528863,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642040269","type":"print"},{"value":"9783642040276","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-04027-6_17","type":"book-chapter","created":{"date-parts":[[2009,9,14]],"date-time":"2009-09-14T17:27:52Z","timestamp":1252949272000},"page":"209-224","source":"Crossref","is-referenced-by-count":4,"title":["Intersection, Universally Quantified, and Reference Types"],"prefix":"10.1007","author":[{"given":"Mariangiola","family":"Dezani-Ciancaglini","sequence":"first","affiliation":[]},{"given":"Paola","family":"Giannini","sequence":"additional","affiliation":[]},{"given":"Simona Ronchi","family":"Della Rocca","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/BFb0022505","volume-title":"Mathematical Foundations of Computer Science 1980","author":"M. Coppo","year":"1980","unstructured":"Coppo, M.: An Extended Polymorphic Type System for Applicative Languages. In: Dembinski, P. (ed.) MFCS 1980. LNCS, vol.\u00a088, pp. 194\u2013204. Springer, Heidelberg (1980)"},{"issue":"4","key":"17_CR2","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M. Coppo","year":"1980","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: An Extension of the Basic Functionality Theory for the \u03bb-calculus. Notre Dame Journal of Formal Logic\u00a021(4), 685\u2013693 (1980)","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"17_CR3","series-title":"SIGPLAN Notices","first-page":"198","volume-title":"ICFP 2000","author":"R. Davies","year":"2000","unstructured":"Davies, R., Pfenning, F.: Intersection Types and Computational Effects. In: Wadler, P. (ed.) ICFP 2000. SIGPLAN Notices, vol.\u00a035(9), pp. 198\u2013208. ACM Press, New York (2000)"},{"key":"17_CR4","unstructured":"Dezani-Ciancaglini, M., Ronchi Della Rocca, S.: Intersection and Reference Types. In: Barendsen, E., Capretta, V., Geuvers, H., Niqui, M. (eds.) Reflections on Type Theory, Lambda Calculus, and the Mind, pp. 77\u201386. Radboud University Nijmegen (2007)"},{"key":"17_CR5","unstructured":"Girard, J.-Y.: Interpr\u00e9tation Fonctionnelle et Elimination des Coupures de l\u2019Arithm\u00e9tique d\u2019Ordre Sup\u00e9rieur. Th\u00e8se d\u2019Etat, Universit\u00e9 de Paris VII (1972)"},{"key":"17_CR6","first-page":"88","volume-title":"POPL 1983","author":"D. Leivant","year":"1983","unstructured":"Leivant, D.: Polymorphic Type Inference. In: Demers, A., Teitelbaum, T. (eds.) POPL 1983, pp. 88\u201398. ACM Press, New York (1983)"},{"key":"17_CR7","unstructured":"Lucassen, J.M.: Types and Effects: Towards the Integration of Functional and Imperative Programming. Ph. d. thesis, Massachusets Institute of Technology (1987)"},{"issue":"3","key":"17_CR8","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1093\/logcom\/5.3.367","volume":"5","author":"I. Margaria","year":"1995","unstructured":"Margaria, I., Zacchi, M.: Principal Typing in a \u2200\u2009\u2227-Discipline. Journal of Logic and Computation\u00a05(3), 367\u2013381 (1995)","journal-title":"Journal of Logic and Computation"},{"issue":"2\/3","key":"17_CR9","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/0890-5401(88)90009-0","volume":"76","author":"J. Mitchell","year":"1988","unstructured":"Mitchell, J.: Polymorphic Type Inference and Containment. Information and Computation\u00a076(2\/3), 211\u2013249 (1988)","journal-title":"Information and Computation"},{"key":"17_CR10","volume-title":"Types and Programming Languages","author":"B.C. Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"17_CR11","first-page":"561","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"G. Pottinger","year":"1980","unstructured":"Pottinger, G.: A Type Assignment for the Strongly Normalizable \u03bb-terms. In: Hindley, R., Seldin, J.P. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561\u2013577. Academic Press, London (1980)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1007\/3-540-06859-7_148","volume-title":"Colloque sur la Programmation","author":"J.C. Reynolds","year":"1974","unstructured":"Reynolds, J.C.: Towards a Theory of Type Structure. In: Loecks, J. (ed.) Colloque sur la Programmation. LNCS, vol.\u00a019, pp. 408\u2013425. Springer, Heidelberg (1974)"},{"issue":"1","key":"17_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.2001.2950","volume":"179","author":"J. Tiuryn","year":"2002","unstructured":"Tiuryn, J., Urzyczyn, P.: The Subtyping Problem for Second-Order Types Is Undecidable. Information and Computation\u00a0179(1), 1\u201318 (2002)","journal-title":"Information and Computation"},{"issue":"1-3","key":"17_CR14","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/S0168-0072(98)00047-5","volume":"98","author":"J.B. Wells","year":"1999","unstructured":"Wells, J.B.: Typability and Type Checking in System F are Equivalent and Undecidable. Annals of Pure and Applied Logic\u00a098(1-3), 111\u2013156 (1999)","journal-title":"Annals of Pure and Applied Logic"},{"key":"17_CR15","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A.K. Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A Syntactic Approach to Type Soundness. Information and Computation\u00a0115, 38\u201394 (1994)","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04027-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T19:47:37Z","timestamp":1552160857000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04027-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642040269","9783642040276"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04027-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}