{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T10:05:11Z","timestamp":1781172311018,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642153747","type":"print"},{"value":"9783642153754","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15375-4_16","type":"book-chapter","created":{"date-parts":[[2010,8,20]],"date-time":"2010-08-20T14:04:18Z","timestamp":1282313058000},"page":"222-236","source":"Crossref","is-referenced-by-count":157,"title":["Session Types as Intuitionistic Linear Propositions"],"prefix":"10.1007","author":[{"given":"Lu\u00eds","family":"Caires","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Abramsky, S.: Computational Interpretations of Linear Logic. TCS\u00a0111(1&2) (1993)","DOI":"10.1016\/0304-3975(93)90181-R"},{"issue":"3","key":"16_CR2","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J.-M. Andreoli","year":"1992","unstructured":"Andreoli, J.-M.: Logic Programming with Focusing Proofs in Linear Logic. Journal of Logic and Computation\u00a02(3), 197\u2013347 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"16_CR3","unstructured":"Barber, A., Plotkin, G.: Dual Intuitionistic Linear Logic. Technical Report LFCS-96-347, Univ. of Edinburgh (1997)"},{"key":"16_CR4","first-page":"147","volume":"155","author":"E. Beffara","year":"2006","unstructured":"Beffara, E.: A Concurrent Model for Linear Logic. ENTCS\u00a0155, 147\u2013168 (2006)","journal-title":"ENTCS"},{"key":"16_CR5","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/0304-3975(94)00104-9","volume":"135","author":"G. Bellin","year":"1994","unstructured":"Bellin, G., Scott, P.: On the \u03c0-Calculus and Linear Logic. TCS\u00a0135, 11\u201365 (1994)","journal-title":"TCS"},{"issue":"2","key":"16_CR6","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1017\/S095679680400543X","volume":"15","author":"E. Bonelli","year":"2005","unstructured":"Bonelli, E., Compagnoni, A., Gunter, E.L.: Correspondence Assertions for Process Synchronization in Concurrent Communications. J. of Func. Prog.\u00a015(2), 219\u2013247 (2005)","journal-title":"J. of Func. Prog."},{"issue":"2","key":"16_CR7","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1016\/S0304-3975(97)00220-X","volume":"195","author":"M. Boreale","year":"1998","unstructured":"Boreale, M.: On the Expressiveness of Internal Mobility in Name-Passing Calculi. Theoretical Computer Science\u00a0195(2), 205\u2013226 (1998)","journal-title":"Theoretical Computer Science"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-73859-6_2","volume-title":"Algebra and Coalgebra in Computer Science","author":"L. Caires","year":"2007","unstructured":"Caires, L.: Logical semantics of types for concurrency. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol.\u00a04624, pp. 16\u201335. Springer, Heidelberg (2007)"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Pfenning, F.: A Linear Logical Framework. Inf. & Comput.\u00a0179(1) (2002)","DOI":"10.1006\/inco.2001.2951"},{"key":"16_CR10","unstructured":"Chang, B.-Y.E., Chaudhuri, K., Pfenning, F.: A Judgmental Analysis of Linear Logic. Technical Report CMU-CS-03-131R, Carnegie Mellon University (2003)"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"6th Intl. Workshop on Web Services and Formal Methods WS-FM 2009","author":"M. Dezani-Ciancaglini","year":"2010","unstructured":"Dezani-Ciancaglini, M., de\u2019 Liguoro, U.: Sessions and Session Types: an Overview. In: 6th Intl. Workshop on Web Services and Formal Methods WS-FM 2009. LNCS. Springer, Heidelberg (2010)"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-540-78663-4_18","volume-title":"Trustworthy Global Computing","author":"M. Dezani-Ciancaglini","year":"2008","unstructured":"Dezani-Ciancaglini, M., de\u2019 Liguoro, U., Yoshida, N.: On Progress for Structured Communications. In: Barthe, G., Fournet, C. (eds.) TGC 2007 and FODO 2008. LNCS, vol.\u00a04912, pp. 257\u2013275. Springer, Heidelberg (2008)"},{"issue":"2-3","key":"16_CR13","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s00236-005-0177-z","volume":"42","author":"S. Gay","year":"2005","unstructured":"Gay, S., Hole, M.: Subtyping for Session Types in the Pi Calculus. Acta Informatica\u00a042(2-3), 191\u2013225 (2005)","journal-title":"Acta Informatica"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0014972","volume-title":"TAPSOFT \u201987 Proceedings of the International Joint Conference on Theory and Practice of Software Development, Pisa, Italy, March 23 - 27 1987.","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y., Lafont, Y.: Linear Logic and Lazy Computation. In: Ehrig, H., Kowalski, R.A., Levi, G., Montanari, U. (eds.) TAPSOFT 1987 and CFLP 1987. LNCS, vol.\u00a0250, pp. 52\u201366. Springer, Heidelberg (1987)"},{"key":"16_CR15","volume-title":"21st International Conference on Concurrency Theory, Concur 2010","author":"M. Giunti","year":"2010","unstructured":"Giunti, M., Vasconcelos, V.T.: A Linear Account of Session Types in the Pi-Calculus. In: Gastin, P., Laroussinie, F. (eds.) 21st International Conference on Concurrency Theory, Concur 2010. Springer, Heidelberg (2010)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1007\/3-540-57208-2_35","volume-title":"CONCUR\u201993","author":"K. Honda","year":"1993","unstructured":"Honda, K.: Types for Dyadic Interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol.\u00a0715, pp. 509\u2013523. Springer, Heidelberg (1993)"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Honda, K., Laurent, O.: An Exact Correspondence between a Typed pi-calculus and Polarised Proof-Nets. Theoretical Computer Science (to appear, 2010)","DOI":"10.1016\/j.tcs.2010.01.028"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/BFb0053567","volume-title":"Programming Languages and Systems","author":"K. Honda","year":"1998","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language Primitives and Type Discipline for Structured Communication-Based Programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol.\u00a01381, pp. 122\u2013138. Springer, Heidelberg (1998)"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Hyland, J.M.E., Luke Ong, C.-H.: Pi-Calculus, Dialogue Games and PCF. In: WG2.8 Conference on Functional Programming Languages, pp. 96\u2013107 (1995)","DOI":"10.1145\/224164.224189"},{"issue":"2","key":"16_CR20","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1145\/276393.278524","volume":"20","author":"N. Kobayashi","year":"1998","unstructured":"Kobayashi, N.: A Partially Deadlock-Free Typed Process Calculus. ACM Tr. Progr. Lang. Sys.\u00a020(2), 436\u2013482 (1998)","journal-title":"ACM Tr. Progr. Lang. Sys."},{"key":"16_CR21","first-page":"358","volume-title":"23rd Symp. on Principles of Programming Languages, POPL 1996","author":"N. Kobayashi","year":"1996","unstructured":"Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the Pi-Calculus. In: 23rd Symp. on Principles of Programming Languages, POPL 1996, pp. 358\u2013371. ACM, New York (1996)"},{"issue":"2","key":"16_CR22","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1017\/S0960129500001407","volume":"2","author":"R. Milner","year":"1992","unstructured":"Milner, R.: Functions as processes. Math. Struc. in Computer Sciences\u00a02(2), 119\u2013141 (1992)","journal-title":"Math. Struc. in Computer Sciences"},{"issue":"1&2","key":"16_CR23","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0304-3975(96)00075-8","volume":"167","author":"D. Sangiorgi","year":"1996","unstructured":"Sangiorgi, D.: Pi-Calculus, Internal Mobility, and Agent Passing Calculi. Theoretical Computer Science\u00a0167(1&2), 235\u2013274 (1996)","journal-title":"Theoretical Computer Science"},{"key":"16_CR24","unstructured":"Sangiorgi, D., Walker, D.: The \u03c0-calculus: A Theory of Mobile Processes. CUP, Cambridge (2001)"},{"key":"16_CR25","unstructured":"Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: Specifying properties of concurrent computations in CLF. In: Sch\u00fcrmann, C. (ed.) 4th Intl. Workshop on Logical Frameworks and Meta-Languages (LFM 2004), Cork, Ireland, July 2004. ENTCS, vol.\u00a0199 (2004)"},{"issue":"2","key":"16_CR26","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/j.jlap.2007.02.011","volume":"72","author":"N. Yoshida","year":"2007","unstructured":"Yoshida, N., Honda, K., Berger, M.: Linearity and Bisimulation. J. Logic and Algebraic Programming\u00a072(2), 207\u2013238 (2007)","journal-title":"J. Logic and Algebraic Programming"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2010 - Concurrency Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15375-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T17:18:42Z","timestamp":1558286322000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15375-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642153747","9783642153754"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15375-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}