{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:13:47Z","timestamp":1775873627649,"version":"3.50.1"},"reference-count":36,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T00:00:00Z","timestamp":1415577600000},"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,3]]},"abstract":"<jats:p>Throughout the years, several typing disciplines for the \u03c0-calculus have been proposed. Arguably, the most widespread of these typing disciplines consists of session types. Session types describe the input\/output behaviour of processes and traditionally provide strong guarantees about this behaviour (i.e. deadlock-freedom and fidelity). While these systems exploit a fundamental notion of linearity, the precise connection between linear logic and session types has not been well understood.<\/jats:p><jats:p>This paper proposes a type system for the \u03c0-calculus that corresponds to a standard sequent calculus presentation of intuitionistic linear logic, interpreting linear propositions as session types and thus providing a purely logical account of all key features and properties of session types. We show the deep correspondence between linear logic and session types by exhibiting a tight operational correspondence between cut-elimination steps and process reductions. We also discuss an alternative presentation of linear session types based on classical linear logic, and compare our development with other more traditional session type systems.<\/jats:p>","DOI":"10.1017\/s0960129514000218","type":"journal-article","created":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T07:01:18Z","timestamp":1415602878000},"page":"367-423","source":"Crossref","is-referenced-by-count":85,"title":["Linear logic propositions as session types"],"prefix":"10.1017","volume":"26","author":[{"given":"LU\u00cdS","family":"CAIRES","sequence":"first","affiliation":[]},{"given":"FRANK","family":"PFENNING","sequence":"additional","affiliation":[]},{"given":"BERNARDO","family":"TONINHO","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,11,10]]},"reference":[{"key":"S0960129514000218_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_30"},{"key":"S0960129514000218_ref33","doi-asserted-by":"crossref","unstructured":"Toninho B. , Caires L. and Pfenning F. (2012) Functions as session-typed processes. In: 15th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'12) 346\u2013360.","DOI":"10.1007\/978-3-642-28729-9_23"},{"key":"S0960129514000218_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00220-X"},{"key":"S0960129514000218_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014972"},{"key":"S0960129514000218_ref29","doi-asserted-by":"crossref","unstructured":"Pfenning F. , Caires L. and Toninho B. (2011) Proof-carrying code in a session-typed process calculus. Certified Programs and Proofs (CPP'11) 21\u201336.","DOI":"10.1007\/978-3-642-25379-9_4"},{"key":"S0960129514000218_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.11.013"},{"key":"S0960129514000218_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004323"},{"key":"S0960129514000218_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"S0960129514000218_ref9","unstructured":"Caires L. , P\u00e9rez J. A. , Pfenning F. and Toninho B. (2012) Relational parametricity for polymorphic session types, Technical Report CMU-CS-12-108, Carnegie Mellon University."},{"key":"S0960129514000218_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680400543X"},{"key":"S0960129514000218_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78663-4_18"},{"key":"S0960129514000218_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/276393.278524"},{"key":"S0960129514000218_ref31","volume-title":"The \u03c0-Calculus: A Theory of Mobile Processes","author":"Sangiorgi","year":"2001"},{"key":"S0960129514000218_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.01.028"},{"key":"S0960129514000218_ref3","unstructured":"Barber A. (1997) Dual intuitionistic linear logic, Technical Report LFCS-96-347, University of Edinburgh."},{"key":"S0960129514000218_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"S0960129514000218_ref23","unstructured":"Hyland J. M. E. and Ong C.-H. L. (1995) Pi-calculus, dialogue games and PCF. In: WG2.8 Conference on Functional Programming Languages 96\u2013107."},{"key":"S0960129514000218_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.055"},{"key":"S0960129514000218_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73859-6_2"},{"key":"S0960129514000218_ref2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"S0960129514000218_ref34","doi-asserted-by":"crossref","unstructured":"Wadler P. (2012) Propositions as sessions. In: Proceedings of the 17th International Conference on Functional Programming, ICFP'12 273\u2013286.","DOI":"10.1145\/2364527.2364568"},{"key":"S0960129514000218_ref11","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.38.4"},{"key":"S0960129514000218_ref13","unstructured":"Chang B.-Y. E. , Chaudhuri K. and Pfenning F. (2003) A judgmental analysis of linear logic, Technical Report CMU-CS-03-131R, Carnegie Mellon University."},{"key":"S0960129514000218_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00104-9"},{"key":"S0960129514000218_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.02.011"},{"key":"S0960129514000218_ref27","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001407"},{"key":"S0960129514000218_ref28","unstructured":"P\u00e9rez J. A. , Caires L. , Pfenning F. and Toninho B. (2012) Termination in session-based concurrency via linear logical relations. In: 22nd European Symposium on Programming (ESOP'12) 539\u2013558."},{"key":"S0960129514000218_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"S0960129514000218_ref30","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00075-8"},{"key":"S0960129514000218_ref25","first-page":"358","volume-title":"23rd Symposium on Principles of Programming Languages (POPL'96)","author":"Kobayashi","year":"1996"},{"key":"S0960129514000218_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"S0960129514000218_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129514000218_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14458-5_1"},{"key":"S0960129514000218_ref12","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2951"},{"key":"S0960129514000218_ref32","doi-asserted-by":"crossref","unstructured":"Toninho B. , Caires L. and Pfenning F. (2011) Dependent session types via intuitionistic linear type theory. In: Principles and Practice of Declarative Programming (PPDP'11), 161\u2013172.","DOI":"10.1145\/2003476.2003499"},{"key":"S0960129514000218_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000218","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T17:02:39Z","timestamp":1555693359000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000218\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,10]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["S0960129514000218"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000218","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,10]]}}}