{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:19Z","timestamp":1775790739602,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642288685","type":"print"},{"value":"9783642288692","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28869-2_27","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:44:36Z","timestamp":1332449076000},"page":"539-558","source":"Crossref","is-referenced-by-count":23,"title":["Linear Logical Relations for Session-Based Concurrency"],"prefix":"10.1007","author":[{"given":"Jorge A.","family":"P\u00e9rez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lu\u00eds","family":"Caires","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernardo","family":"Toninho","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(93)90181-R","volume":"111","author":"S. Abramsky","year":"1993","unstructured":"Abramsky, S.: Computational interpretations of linear logic. Theor. Comput. Sci.\u00a0111, 3\u201357 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"27_CR2","unstructured":"Barber, A.: Dual intuitionistic linear logic. Technical report, LFCS-96-347, Univ. of Edinburgh (1996)"},{"key":"27_CR3","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. Theor. Comput. Sci.\u00a0195, 205\u2013226 (1998)","journal-title":"Theor. Comput. Sci."},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-642-15375-4_16","volume-title":"CONCUR 2010 - Concurrency Theory","author":"L. Caires","year":"2010","unstructured":"Caires, L., Pfenning, F.: Session Types as Intuitionistic Linear Propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 222\u2013236. Springer, Heidelberg (2010)"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"Caires, L., Pfenning, F., Toninho, B.: Towards concurrent type theory. In: Proc. of 7th Workshop on Types in Language Design and Implementation \u2013 TLDI 2012 (2012)","DOI":"10.1145\/2103786.2103788"},{"key":"27_CR6","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":"27_CR7","doi-asserted-by":"crossref","unstructured":"Dal Lago, U., Di Giamberardino, P.: Soft session types. In: Proc. of 18th Workshop on Expressiveness in Concurrency \u2013 EXPRESS 2011. EPTCS, vol.\u00a064, pp. 59\u201373 (2011)","DOI":"10.4204\/EPTCS.64.5"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-642-04164-8_13","volume-title":"Semantics and Algebraic Specification","author":"R. Demangeon","year":"2009","unstructured":"Demangeon, R., Hirschkoff, D., Sangiorgi, D.: Mobile Processes and Termination. In: Palsberg, J. (ed.) Mosses Festschrift. LNCS, vol.\u00a05700, pp. 250\u2013273. Springer, Heidelberg (2009)"},{"issue":"5","key":"27_CR9","doi-asserted-by":"publisher","first-page":"825","DOI":"10.1017\/S0960129505004871","volume":"15","author":"R. Di Cosmo","year":"2005","unstructured":"Di Cosmo, R.: A short survey of isomorphisms of types. Mathematical Structures in Computer Science\u00a015(5), 825\u2013838 (2005)","journal-title":"Mathematical Structures in Computer Science"},{"key":"27_CR10","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., Levi, G., Montanari, U. (eds.) TAPSOFT 1987. LNCS, vol.\u00a0250, pp. 52\u201366. Springer, Heidelberg (1987)"},{"key":"27_CR11","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":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/978-3-540-70592-5_22","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","author":"R. Hu","year":"2008","unstructured":"Hu, R., Yoshida, N., Honda, K.: Session-Based Distributed Programming in Java. In: Ryan, M. (ed.) ECOOP 2008. LNCS, vol.\u00a05142, pp. 516\u2013541. Springer, Heidelberg (2008)"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. In: POPL, pp. 358\u2013371 (1996)","DOI":"10.1145\/237721.237804"},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-21461-5_15","volume-title":"Formal Techniques for Distributed Systems","author":"D. Kouzapas","year":"2011","unstructured":"Kouzapas, D., Yoshida, N., Honda, K.: On Asynchronous Session Semantics. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol.\u00a06722, pp. 228\u2013243. Springer, Heidelberg (2011)"},{"issue":"1-2","key":"27_CR15","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.tcs.2003.10.018","volume":"318","author":"Y. Lafont","year":"2004","unstructured":"Lafont, Y.: Soft linear logic and polynomial time. Theor. Comput. Sci.\u00a0318(1-2), 163\u2013180 (2004)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"27_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, part I\/II. Inf. Comput.\u00a0100(1), 1\u201377 (1992)","journal-title":"Inf. Comput."},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-642-21464-6_8","volume-title":"Coordination Models and Languages","author":"N. Ng","year":"2011","unstructured":"Ng, N., Yoshida, N., Pernet, O., Hu, R., Kryftis, Y.: Safe Parallel Programming with Session Java. In: De Meuter, W., Roman, G.-C. (eds.) COORDINATION 2011. LNCS, vol.\u00a06721, pp. 110\u2013126. Springer, Heidelberg (2011)"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"P\u00e9rez, J.A., Caires, L., Pfenning, F., Toninho, B.: Linear Logical Relations for Session-Based Concurrency, Extended Version (2012), \n                  \n                    http:\/\/goo.gl\/iQVZu","DOI":"10.1007\/978-3-642-28869-2_27"},{"key":"27_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-25379-9_4","volume-title":"Certified Programs and Proofs","author":"F. Pfenning","year":"2011","unstructured":"Pfenning, F., Caires, L., Toninho, B.: Proof-Carrying Code in a Session-Typed Process Calculus. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 21\u201336. Springer, Heidelberg (2011)"},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"Pucella, R., Tov, J.A.: Haskell session types with (almost) no class. In: Proc. of ACM SIGPLAN Symposium on Haskell, pp. 25\u201336. ACM (2008)","DOI":"10.1145\/1411286.1411290"},{"issue":"1","key":"27_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0960129505004810","volume":"16","author":"D. Sangiorgi","year":"2006","unstructured":"Sangiorgi, D.: Termination of processes. Mathematical Structures in Computer Science\u00a016(1), 1\u201339 (2006)","journal-title":"Mathematical Structures in Computer Science"},{"key":"27_CR22","volume-title":"The \u03c0-calculus: A Theory of Mobile Processes","author":"D. Sangiorgi","year":"2001","unstructured":"Sangiorgi, D., Walker, D.: The \u03c0-calculus: A Theory of Mobile Processes. Cambridge University Press, New York (2001)"},{"issue":"2\/3","key":"27_CR23","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0019-9958(85)80001-2","volume":"65","author":"R. Statman","year":"1985","unstructured":"Statman, R.: Logical relations and the typed lambda-calculus. Information and Control\u00a065(2\/3), 85\u201397 (1985)","journal-title":"Information and Control"},{"key":"27_CR24","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"Tait, W.W.: Intensional Interpretations of Functionals of Finite Type I. J. Symbolic Logic\u00a032, 198\u2013212 (1967)","journal-title":"J. Symbolic Logic"},{"key":"27_CR25","first-page":"161","volume-title":"Proc. of PPDP 2011","author":"B. Toninho","year":"2011","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: Proc. of PPDP 2011, pp. 161\u2013172. ACM Press, New York (2011)"},{"issue":"2","key":"27_CR26","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/j.ic.2003.08.004","volume":"191","author":"N. Yoshida","year":"2004","unstructured":"Yoshida, N., Berger, M., Honda, K.: Strong normalisation in the pi -calculus. Inf. Comput.\u00a0191(2), 145\u2013202 (2004)","journal-title":"Inf. Comput."},{"issue":"2","key":"27_CR27","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. Log. Algebr. Program.\u00a072(2), 207\u2013238 (2007)","journal-title":"J. Log. Algebr. Program."}],"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_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:13:43Z","timestamp":1620126823000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28869-2_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288685","9783642288692"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28869-2_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}