{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:27Z","timestamp":1760202687604,"version":"3.40.5"},"reference-count":16,"publisher":"Cambridge University Press (CUP)","issue":"8","license":[{"start":{"date-parts":[[2015,1,14]],"date-time":"2015-01-14T00:00:00Z","timestamp":1421193600000},"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":[[2016,12]]},"abstract":"<jats:p>We show how systems of session types can enforce interactions to take bounded time for all typable processes. The type system we propose is based on Lafont's soft linear logic and is strongly inspired by recent works about session types as intuitionistic linear logic formulas. Our main result is the existence, for every typable process, of a polynomial bound on the length of reduction sequences starting from it and on the size of its reducts.<\/jats:p>","DOI":"10.1017\/s0960129514000632","type":"journal-article","created":{"date-parts":[[2015,1,14]],"date-time":"2015-01-14T07:15:14Z","timestamp":1421219714000},"page":"1433-1458","source":"Crossref","is-referenced-by-count":2,"title":["On session types and polynomial time"],"prefix":"10.1017","volume":"26","author":[{"given":"UGO","family":"DAL LAGO","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"PAOLO","family":"DI GIAMBERARDINO","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2015,1,14]]},"reference":[{"key":"S0960129514000632_ref6","first-page":"717","article-title":"On light logics, uniform encodings and polynomial time","volume":"16","author":"Dal Lago","year":"2006","journal-title":"Mathematical Structures in Computer Science"},{"key":"S0960129514000632_ref12","doi-asserted-by":"crossref","unstructured":"Honda K. , Vasconcelos V. and Kubo M. (1998) Language primitives and type discipline for structured communication-based programming. In: European Symposium on Programming 1998, 122\u2013138.","DOI":"10.1007\/BFb0053567"},{"key":"S0960129514000632_ref11","doi-asserted-by":"crossref","unstructured":"Honda K. , Nobuko Y. and Carbone M. (2008) Multiparty asynchronous session types. In: Principles of Programming Languages 2008, 273\u2013284.","DOI":"10.1145\/1328438.1328472"},{"key":"S0960129514000632_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.045"},{"key":"S0960129514000632_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(79)90007-0"},{"key":"S0960129514000632_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.018"},{"key":"S0960129514000632_ref5","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/978-3-642-25379-9_4","article-title":"Proof-carrying code in a session-typed process calculus","volume":"7086","author":"Caires","year":"2011","journal-title":"Lecture Notes in Computer Science"},{"key":"S0960129514000632_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_19"},{"key":"S0960129514000632_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129514000632_ref8","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.41.4"},{"key":"S0960129514000632_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"S0960129514000632_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24727-2_4"},{"key":"S0960129514000632_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73228-0_23"},{"key":"S0960129514000632_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90020-G"},{"key":"S0960129514000632_ref7","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.64.5"},{"key":"S0960129514000632_ref4","doi-asserted-by":"crossref","unstructured":"Caires L. , Pfenning F. and Toninho B. (2011a) Dependent session types via intuitionistic linear type theory. In: International Symposium on Principles and Practice of Declarative Programming 2011, 161\u2013172.","DOI":"10.1145\/2003476.2003499"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000632","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,16]],"date-time":"2025-05-16T21:52:31Z","timestamp":1747432351000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000632\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,14]]},"references-count":16,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2016,12]]}},"alternative-id":["S0960129514000632"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000632","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2015,1,14]]}}}