{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:41Z","timestamp":1751660501088,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540433637"},{"type":"electronic","value":"9783540459279"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","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":[[2002]]},"DOI":"10.1007\/3-540-45927-8_9","type":"book-chapter","created":{"date-parts":[[2007,10,19]],"date-time":"2007-10-19T09:39:04Z","timestamp":1192786744000},"page":"115-132","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Branching Types"],"prefix":"10.1007","author":[{"given":"Joe B.","family":"Wells","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Haack","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"9_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1007\/3-540-46425-5_2","volume-title":"Faithful translations between polyvariant flows and polymorphic types","author":"T. Amtoft","year":"2000","unstructured":"T. Amtoft, F. Turbak. Faithful translations between polyvariant flows and polymorphic types. In Programming Languages & Systems, 9th European Symp. Programming, vol. 1782 of LNCS, pp. 26\u201340. Springer-Verlag, 2000."},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"B. Capitani, M. Loreti, B. Venneri. Hyperformulae, parallel deductions and intersection types. Electronic Notes in Theoretical Computer Science, 50, 2001. Proceedings of ICALP 2001 workshop: Bohm\u2019s Theorem: Applications to Computer Science Theory (BOTH 2001), Crete, Greece, 2001-07-13.","DOI":"10.1016\/S1571-0661(04)00172-0"},{"issue":"4","key":"9_CR3","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M. Coppo","year":"1980","unstructured":"M. Coppo, M. Dezani-Ciancaglini. An extension of the basic functionality theory for the \u03bb-calculus. Notre Dame J. Formal Logic, 21(4):685\u2013693, 1980.","journal-title":"Notre Dame J. Formal Logic"},{"issue":"2","key":"9_CR4","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1305\/ndjfl\/1039724889","volume":"38","author":"M. Dezani-Ciancaglini","year":"1997","unstructured":"M. Dezani-Ciancaglini, S. Ghilezan, B. Venneri. The \u201crelevance\u201d of intersection and union types. Notre Dame J. Formal Logic, 38(2):246\u2013269, Spring 1997.","journal-title":"Notre Dame J. Formal Logic"},{"key":"9_CR5","unstructured":"A. Dimock, R. Muller, F. Turbak, J. B. Wells. Strongly typed flow-directed representation transformations. In Proc. 1997 Int\u2019l Conf. Functional Programming, pp. 11\u201324. ACM Press, 1997."},{"key":"9_CR6","unstructured":"A. Dimock, I. Westmacott, R. Muller, F. Turbak, J. B. Wells. Functioning without closure: Type-safe customized function representations for Standard ML. In Proc. 2001 Int\u2019l Conf. Functional Programming, pp. 14\u201325. ACM Press, 2001."},{"key":"9_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/3-540-45332-6_2","volume-title":"Program representation size in an intermediate language with intersection and union types","author":"A. Dimock","year":"2001","unstructured":"A. Dimock, I. Westmacott, R. Muller, F. Turbak, J. B. Wells, J. Considine. Program representation size in an intermediate language with intersection and union types. In Proceedings of the Third Workshop on Types in Compilation (TIC 2000), vol. 2071 of LNCS, pp. 27\u201352. Springer-Verlag, 2001."},{"key":"9_CR8","unstructured":"J.-Y. Girard. 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":"9_CR9","unstructured":"A. J. Kfoury. A linearization of the lambda-calculus. J. Logic Comput., 10(3), 2000. Special issue on Type Theory and Term Rewriting. Kamareddine and Klop (editors)."},{"key":"9_CR10","unstructured":"A. J. Kfoury, H. G. Mairson, F. A. Turbak, J. B. Wells. Relating typability and expressibility in finite-rank intersection type systems. In Proc. 1999 Int\u2019l Conf. Functional Programming, pp. 90\u2013101. ACM Press, 1999."},{"key":"9_CR11","unstructured":"A. J. Kfoury, J. B. Wells. A direct algorithm for type inference in the rank-2 fragment of the second-order \u03bb-calculus. In Proc. 1994 ACM Conf. LISP Funct. Program., pp. 196\u2013207, 1994."},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"A. J. Kfoury, J. B. Wells. Principality and decidable type inference for finite-rank intersection types. In Conf. Rec. POPL\u2019 99: 26th ACM Symp. Princ. of Prog. Langs., pp. 161\u2013174, 1999.","DOI":"10.1145\/292540.292556"},{"issue":"3","key":"9_CR13","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1017\/S095679680100394X","volume":"11","author":"J. Palsberg","year":"2001","unstructured":"J. Palsberg, C. Pavlopoulou. From polyvariant flow information to intersection and union types. J. Funct. Programming, 11(3):263\u2013317, May 2001.","journal-title":"J. Funct. Programming"},{"key":"9_CR14","unstructured":"B. C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, Feb. 1991."},{"key":"9_CR15","unstructured":"G. Pottinger. A type assignment for the strongly normalizable \u03bb-terms. In J. R. Hindley, J. P. Seldin, eds., To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp. 561\u2013577. Academic Press, 1980."},{"key":"9_CR16","series-title":"Lect Notes Comput Sci","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":"J. C. Reynolds. Towards a theory of type structure. In Colloque sur la Programmation, vol. 19 of LNCS, pp. 408\u2013425, Paris, France, 1974. Springer-Verlag."},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"J. C. Reynolds. Design of the programming language Forsythe. In P. O\u2019Hearn, R. D. Tennent, eds., Algol-like Languages. Birkhauser, 1996.","DOI":"10.1007\/978-1-4612-4118-8_9"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"S. Ronchi Della Rocca, L. Roversi. Intersection logic. In Computer Science Logic, CSL\u2019 01. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-44802-0_29"},{"key":"9_CR19","unstructured":"F. Turbak, A. Dimock, R. Muller, J. B. Wells. Compiling with polymorphic and polyvariant flow types. In Proc. First Int\u2019l Workshop on Types in Compilation, June 1997."},{"issue":"4","key":"9_CR20","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1017\/S0960129597002302","volume":"7","author":"P. Urzyczyn","year":"1997","unstructured":"P. Urzyczyn. Type reconstruction in F \u03c9. Math. Structures Comput. Sci., 7(4):329\u2013358, 1997.","journal-title":"Math. Structures Comput. Sci."},{"issue":"2","key":"9_CR21","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1093\/logcom\/4.2.109","volume":"4","author":"B. Venneri","year":"1994","unstructured":"B. Venneri. Intersection types as logical formulae. J. Logic Comput., 4(2):109\u2013124, Apr. 1994.","journal-title":"J. Logic Comput."},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"J. B. Wells. Typability and type checking in the second-order \u03bb-calculus are equivalent and undecidable. In Proc. 9th Ann. IEEE Symp. Logic in Comp. Sci., pp. 176\u2013185, 1994. Superseded by [24].","DOI":"10.1109\/LICS.1994.316068"},{"key":"9_CR23","unstructured":"J. B. Wells. Typability is undecidable for F+eta. Tech. Rep. 96-022, Comp. Sci. Dept., Boston Univ., Mar. 1996."},{"issue":"1","key":"9_CR24","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/S0168-0072(98)00047-5","volume":"98","author":"J. B. Wells","year":"1999","unstructured":"J. B. Wells. Typability and type checking in System F are equivalent and undecidable. Ann. Pure Appl. Logic, 98(1\u20133):111\u2013156, 1999. Supersedes [22].","journal-title":"Ann. Pure Appl. Logic"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"J. B. Wells, A. Dimock, R. Muller, F. Turbak. A typed intermediate language for flow-directed compilation. In Proc. 7th Int\u2019l Joint Conf. Theory & Practice of Software Development, pp. 757\u2013771, 1997. Superseded by [26].","DOI":"10.1007\/BFb0030639"},{"key":"9_CR26","unstructured":"J. B. Wells, A. Dimock, R. Muller, F. Turbak. A calculus with polymorphic and polyvariant flow types. J. Funct. Programming, 200X. To appear. Supersedes [25]."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45927-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T19:13:56Z","timestamp":1737486836000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45927-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540433637","9783540459279"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-45927-8_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"14 March 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}