{"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":1751660501621,"version":"3.41.0"},"reference-count":39,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2008,12,1]],"date-time":"2008-12-01T00:00:00Z","timestamp":1228089600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2008,12]]},"abstract":"<jats:p>We describe a polymorphic, typed lambda calculus with substructural features. This calculus extends the first-order substructural lambda calculus \u03b1\u03bb associated with bunched logic. A particular novelty of our new calculus is the substructural treatment of second-order variables. This is accomplished through the use of bunches of type variables in typing contexts. Both additive and multiplicative forms of polymorphic abstraction are then supported. The calculus has sensible proof-theoretic properties and a straightforward categorical semantics using indexed categories. We produce a model for additive polymorphism with first-order bunching based on partial equivalence relations. We consider additive and multiplicative existential quantifiers separately from the universal quantifiers.<\/jats:p>","DOI":"10.1017\/s0960129508007159","type":"journal-article","created":{"date-parts":[[2008,10,7]],"date-time":"2008-10-07T08:59:54Z","timestamp":1223369994000},"page":"1091-1132","source":"Crossref","is-referenced-by-count":8,"title":["Bunched polymorphism"],"prefix":"10.1017","volume":"18","author":[{"given":"MATTHEW","family":"COLLINSON","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"DAVID","family":"PYM","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"EDMUND","family":"ROBINSON","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2008,12,1]]},"reference":[{"key":"S0960129508007159_manual_ref-11","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0060438"},{"key":"S0960129508007159_manual_ref-4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_17"},{"key":"S0960129508007159_manual_ref-28","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"S0960129508007159_manual_ref-32","doi-asserted-by":"crossref","unstructured":"Prawitz, D. (1978) Proofs and the meaning and completeness of logical constants. In: Hintikka, J., Niiniluoto, I. and Saarinen, E. (eds.) Essays on mathematical and philosophical logic, D. Reidel 25\u201340.","DOI":"10.1007\/978-94-009-9825-4_2"},{"key":"S0960129508007159_manual_ref-6","first-page":"1","article-title":"Linear Abadi and Plotkin logic","volume":"5","author":"Birkedal","year":"2006","journal-title":"Logical Methods in Computer Science"},{"volume-title":"Proofs and Types","year":"1989","author":"Girard","key":"S0960129508007159_manual_ref-17"},{"key":"S0960129508007159_manual_ref-19","article-title":"Categorical Logic and Type Theory","volume":"141","author":"Jacobs","year":"1999","journal-title":"Studies in Logic and the Foundations of Mathematics"},{"key":"S0960129508007159_manual_ref-14","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"S0960129508007159_manual_ref-12","article-title":"An embedding theorem for closed categories","volume":"420","author":"Day","year":"1973","journal-title":"Springer-Verlag Lecture Notes in Mathematics"},{"key":"S0960129508007159_manual_ref-29","unstructured":"Oles, F. J. (1982) A Category-Theoretic Approach to the Semantics of Programming Languages, Ph.D. thesis, Syracuse University, Syracuse, U.S.A."},{"key":"S0960129508007159_manual_ref-33","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"S0960129508007159_manual_ref-35","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"S0960129508007159_manual_ref-20","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"key":"S0960129508007159_manual_ref-10","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_5"},{"key":"S0960129508007159_manual_ref-21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"S0960129508007159_manual_ref-25","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90067-V"},{"key":"S0960129508007159_manual_ref-37","first-page":"55","volume-title":"Logic in Computer Science, LICS '02","author":"Reynolds","year":"2002"},{"key":"S0960129508007159_manual_ref-5","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80874-0"},{"key":"S0960129508007159_manual_ref-9","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.010"},{"key":"S0960129508007159_manual_ref-1","first-page":"31","volume-title":"Logic in Computer Science, LICS '90","author":"Abadi","year":"1990"},{"volume-title":"Types and Programming Languages","year":"2002","author":"Pierce","key":"S0960129508007159_manual_ref-30"},{"key":"S0960129508007159_manual_ref-15","unstructured":"Girard, J.-Y. (1972) Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieur, Ph.D. thesis, Universit\u00e9 Paris VII."},{"key":"S0960129508007159_manual_ref-2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_16"},{"key":"S0960129508007159_manual_ref-13","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"key":"S0960129508007159_manual_ref-27","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004495"},{"key":"S0960129508007159_manual_ref-23","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80019-5"},{"key":"S0960129508007159_manual_ref-8","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91586"},{"key":"S0960129508007159_manual_ref-34","article-title":"The Semantics and Proof Theory of the Logic of Bunched Implications","volume":"26","author":"Pym","year":"2002","journal-title":"Applied Logic Series"},{"key":"S0960129508007159_manual_ref-16","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"volume-title":"Sheaves in Geometry and Logic: A First Introduction to Topos Theory","year":"1992","author":"Mac Lane","key":"S0960129508007159_manual_ref-22"},{"key":"S0960129508007159_manual_ref-38","doi-asserted-by":"publisher","DOI":"10.2307\/2273831"},{"key":"S0960129508007159_manual_ref-39","doi-asserted-by":"publisher","DOI":"10.1145\/286860.286882"},{"key":"S0960129508007159_manual_ref-36","first-page":"345","volume-title":"Algorithmic Languages","author":"Reynolds","year":"1981"},{"key":"S0960129508007159_manual_ref-24","unstructured":"Maneggia, P. (2004) Models of linear polymorphism, Ph.D. thesis, School of Computer Science, The University of Birmingham."},{"key":"S0960129508007159_manual_ref-18","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(88)90018-8"},{"key":"S0960129508007159_manual_ref-7","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(2:6)2008"},{"key":"S0960129508007159_manual_ref-26","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"S0960129508007159_manual_ref-31","first-page":"374","volume-title":"Logic in Computer Science, LICS '93","author":"Plotkin","year":"1993"},{"key":"S0960129508007159_manual_ref-3","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.006"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129508007159","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T07:45:17Z","timestamp":1750491917000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129508007159\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12]]},"references-count":39,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2008,2]]}},"alternative-id":["S0960129508007159"],"URL":"https:\/\/doi.org\/10.1017\/s0960129508007159","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2008,12]]}}}