{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T00:47:07Z","timestamp":1725670027419},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642288685"},{"type":"electronic","value":"9783642288692"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28869-2_23","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T16:44:36Z","timestamp":1332434676000},"page":"456-475","source":"Crossref","is-referenced-by-count":1,"title":["Expansion for Universal Quantifiers"],"prefix":"10.1007","author":[{"given":"Sergue\u00ef","family":"Lenglet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joe B.","family":"Wells","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-24725-8_21","volume-title":"Programming Languages and Systems","author":"S. Carlier","year":"2004","unstructured":"Carlier, S., Polakow, J., Wells, J.B., Kfoury, A.J.: System\u00a0E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 294\u2013309. Springer, Heidelberg (2004)"},{"key":"23_CR2","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/j.entcs.2005.03.026","volume":"136","author":"S. Carlier","year":"2005","unstructured":"Carlier, S., Wells, J.B.: Expansion: the crucial mechanism for type inference with intersection types: A survey and explanation. Electr. Notes Theor. Comput. Sci.\u00a0136, 173\u2013202 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"23_CR3","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Principal type schemes and \u03bb-calculus semantics. In: Hindley, J.R., Seldin, J.P. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp. 535\u2013560. Academic Press (1980)"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Damas, L., Milner, R.: Principal type-schemes for functional programs. In: POPL, pp. 207\u2013212 (1982)","DOI":"10.1145\/582153.582176"},{"issue":"1-2","key":"23_CR5","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1006\/inco.1999.2830","volume":"155","author":"J. Garrigue","year":"1999","unstructured":"Garrigue, J., R\u00e9my, D.: Semi-explicit first-class polymorphism for ML. Inf. Comput.\u00a0155(1-2), 134\u2013169 (1999)","journal-title":"Inf. Comput."},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-54415-1_39","volume-title":"Theoretical Aspects of Computer Software","author":"P. Giannini","year":"1991","unstructured":"Giannini, P., Ronchi Della Rocca, S.: Type Inference in Polymorphic Type Discipline. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol.\u00a0526, pp. 18\u201337. Springer, Heidelberg (1991)"},{"key":"23_CR7","unstructured":"Girard, J.-Y.: Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris VII (1972)"},{"issue":"1-3","key":"23_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2003.10.032","volume":"311","author":"A.J. Kfoury","year":"2004","unstructured":"Kfoury, A.J., Wells, J.B.: Principality and type inference for intersection types using expansion variables. Theor. Comput. Sci.\u00a0311(1-3), 1\u201370 (2004)","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"23_CR9","doi-asserted-by":"publisher","first-page":"1411","DOI":"10.1145\/186025.186031","volume":"16","author":"K. L\u00e4ufer","year":"1994","unstructured":"L\u00e4ufer, K., Odersky, M.: Polymorphic type inference and abstract data types. ACM Trans. Program. Lang. Syst.\u00a016(5), 1411\u20131430 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Le Botlan, D., R\u00e9my, D.: MLF: raising ML to the power of System F. In: ICFP, pp. 27\u201338. ACM (2003)","DOI":"10.1145\/944746.944709"},{"issue":"6","key":"23_CR11","doi-asserted-by":"publisher","first-page":"726","DOI":"10.1016\/j.ic.2008.12.006","volume":"207","author":"D. Le Botlan","year":"2009","unstructured":"Le Botlan, D., R\u00e9my, D.: Recasting MLF. Inf. Comput.\u00a0207(6), 726\u2013785 (2009)","journal-title":"Inf. Comput."},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"Leijen, D.: Flexible types: robust type inference for first-class polymorphism. In: POPL, pp. 66\u201377. ACM (2009)","DOI":"10.1145\/1594834.1480891"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Leivant, D.: Polymorphic type inference. In: POPL, pp. 88\u201398 (1983)","DOI":"10.1145\/567067.567077"},{"key":"23_CR14","unstructured":"Lenglet, S., Wells, J.B.: Expansion for universal quantifiers (2012), \n                  \n                    http:\/\/arxiv.org\/abs\/1201.1101"},{"issue":"3","key":"23_CR15","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 forall-and-discipline. J. Log. Comput.\u00a05(3), 367\u2013381 (1995)","journal-title":"J. Log. Comput."},{"issue":"3","key":"23_CR16","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci.\u00a017(3), 348\u2013375 (1978)","journal-title":"J. Comput. Syst. Sci."},{"issue":"2\/3","key":"23_CR17","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/0890-5401(88)90009-0","volume":"76","author":"J.C. Mitchell","year":"1988","unstructured":"Mitchell, J.C.: Polymorphic type inference and containment. Inf. Comput.\u00a076(2\/3), 211\u2013249 (1988)","journal-title":"Inf. Comput."},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/3-540-57887-0_102","volume-title":"Theoretical Aspects of Computer Software","author":"D. R\u00e9my","year":"1994","unstructured":"R\u00e9my, D.: Programming Objects with ML-ART, an Extension to ML with Abstract and Record Types. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol.\u00a0789, pp. 321\u2013346. Springer, Heidelberg (1994)"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1007\/3-540-06859-7_148","volume-title":"Automata, Languages and Programming","author":"J.C. Reynolds","year":"1974","unstructured":"Reynolds, J.C.: Towards a Theory of Type Structure. In: Loeckx, J. (ed.) ICALP 1974. LNCS, vol.\u00a014, pp. 408\u2013423. Springer, Heidelberg (1974)"},{"key":"23_CR20","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/0304-3975(83)90069-5","volume":"28","author":"S. Ronchi Della Rocca","year":"1984","unstructured":"Ronchi Della Rocca, S., Venneri, B.: Principal type schemes for an extended type theory. Theoretical Computer Science\u00a028, 151\u2013169 (1984)","journal-title":"Theoretical Computer Science"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-44557-9_3","volume-title":"Types for Proofs and Programs","author":"S. Bakel van","year":"2000","unstructured":"van Bakel, S., Barbanera, F., Fern\u00e1ndez, M.: Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and \u03b2-Rule. In: Coquand, T., Nordstr\u00f6m, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol.\u00a01956, pp. 41\u201360. Springer, Heidelberg (2000)"},{"issue":"8","key":"23_CR22","first-page":"873","volume":"9","author":"C. Vasconcellos","year":"2003","unstructured":"Vasconcellos, C., Figueiredo, L., Camar\u00e3o, C.: Practical type inference for polymorphic recursion: an implementation in haskell. J. UCS\u00a09(8), 873\u2013890 (2003)","journal-title":"J. UCS"},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"Vytiniotis, D., Weirich, S., Peyton-Jones, S.: FPH: first-class polymorphism for Haskell. In: ICFP, pp. 295\u2013306. ACM (2008)","DOI":"10.1145\/1411203.1411246"},{"key":"23_CR24","doi-asserted-by":"crossref","unstructured":"Vytiniotis, D., Weirich, S., Peyton-Jones, S.: Boxy types: inference for higher-rank types and impredicativity. In: ICFP, pp. 251\u2013262. ACM (2006)","DOI":"10.1145\/1160074.1159838"},{"issue":"1-3","key":"23_CR25","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. Ann. Pure Appl. Logic\u00a098(1-3), 111\u2013156 (1999)","journal-title":"Ann. Pure Appl. Logic"},{"key":"23_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1007\/3-540-45465-9_78","volume-title":"Automata, Languages and Programming","author":"J.B. Wells","year":"2002","unstructured":"Wells, J.B.: The Essence of Principal Typings. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol.\u00a02380, pp. 913\u2013925. Springer, Heidelberg (2002)"},{"key":"23_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/3-540-45927-8_9","volume-title":"Programming Languages and Systems","author":"J.B. Wells","year":"2002","unstructured":"Wells, J.B., Haack, C.: Branching Types. In: Le M\u00e9tayer, D. (ed.) ESOP 2002. LNCS, vol.\u00a02305, pp. 115\u2013132. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28869-2_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:13:41Z","timestamp":1620112421000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28869-2_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288685","9783642288692"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28869-2_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}