{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:25:30Z","timestamp":1740108330872,"version":"3.37.3"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,3,18]],"date-time":"2021-03-18T00:00:00Z","timestamp":1616025600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,18]],"date-time":"2021-03-18T00:00:00Z","timestamp":1616025600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Colciencias ECOS-NORD","award":["Project FACTS (C19M03)"],"award-info":[{"award-number":["Project FACTS (C19M03)"]}]},{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["016.Vidi.189.046"],"award-info":[{"award-number":["016.Vidi.189.046"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100012774","name":"Innovationsfonden","doi-asserted-by":"publisher","award":["Ecoknow.org (705000034A)"],"award-info":[{"award-number":["Ecoknow.org (705000034A)"]}],"id":[{"id":"10.13039\/100012774","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010665","name":"H2020 Marie Sklodowska-Curie Actions","doi-asserted-by":"publisher","award":["778233 (BehAPI)"],"award-info":[{"award-number":["778233 (BehAPI)"]}],"id":[{"id":"10.13039\/100010665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2022,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:italic>Session-based concurrency<\/jats:italic>is a type-based approach to the analysis of message-passing programs. These programs may be specified in an<jats:italic>operational<\/jats:italic>or<jats:italic>declarative<\/jats:italic>style: the former defines how interactions are properly structured; the latter defines governing conditions for correct interactions. In this paper, we study rigorous relationships between operational and declarative models of session-based concurrency. We develop a correct encoding of session<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\pi $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03c0<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus processes into the linear concurrent constraint calculus\u00a0(<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\texttt {lcc}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>lcc<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>), a declarative model of concurrency based on partial information (constraints). We exploit session types to ensure that our encoding satisfies precise correctness properties and that it offers a sound basis on which operational and declarative requirements can be jointly specified and reasoned about. We demonstrate the applicability of our results by using our encoding in the specification of realistic communication patterns with time and contextual information.<\/jats:p>","DOI":"10.1007\/s00236-021-00395-w","type":"journal-article","created":{"date-parts":[[2021,3,18]],"date-time":"2021-03-18T19:38:11Z","timestamp":1616096291000},"page":"1-87","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Session-based concurrency, declaratively"],"prefix":"10.1007","volume":"59","author":[{"given":"Mauricio","family":"Cano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5162-7936","authenticated-orcid":false,"given":"Hugo A.","family":"L\u00f3pez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1452-6180","authenticated-orcid":false,"given":"Jorge A.","family":"P\u00e9rez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8387-9644","authenticated-orcid":false,"given":"Camilo","family":"Rueda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,18]]},"reference":[{"key":"395_CR1","unstructured":"Arslanagic, A., P\u00e9rez, J.A., Voogd, E.: Minimal session types (Pearl). In: 33rd European Conference on Object-Oriented Programming, ECOOP 2019, July 15\u201319, 2019, London, United Kingdom, pp. 23:1\u201323:28 (2019)"},{"issue":"1","key":"395_CR2","first-page":"5","volume":"22","author":"M Bartoletti","year":"2012","unstructured":"Bartoletti, M., Tuosto, E., Zunino, R.: Contract-oriented computing in CO2. Sci. Ann. Comp. Sci. 22(1), 5\u201360 (2012)","journal-title":"Sci. Ann. Comp. Sci."},{"key":"395_CR3","unstructured":"Bartoletti, M., Zunino, R.: A calculus of contracting processes. Technical Report DISI-09-056, University of Trento (2009)"},{"key":"395_CR4","doi-asserted-by":"crossref","unstructured":"Bartoletti, M., Zunino, R.: A calculus of contracting processes. In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11\u201314 July 2010, Edinburgh, United Kingdom, pp. 332\u2013341 (2010)","DOI":"10.1109\/LICS.2010.25"},{"issue":"1","key":"395_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-7(1:11)2011","volume":"7","author":"J Bengtson","year":"2011","unstructured":"Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: a framework for mobile processes with nominal data and logic. Log. Methods Comput. Sci. 7(1), 1\u201344 (2011)","journal-title":"Log. Methods Comput. Sci."},{"key":"395_CR6","doi-asserted-by":"crossref","unstructured":"Bernardi, G., Dardha, O., Gay, S.J., Kouzapas, D.: On duality relations for session types. In: Trustworthy Global Computing\u20149th International Symposium, TGC 2014, Rome, Italy, pp. 51\u201366 (2014)","DOI":"10.1007\/978-3-662-45917-1_4"},{"issue":"2","key":"395_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-12(2:10)2016","volume":"12","author":"G Bernardi","year":"2016","unstructured":"Bernardi, G., Hennessy, M.: Using higher-order contracts to model session types. Log. Methods Comput. Sci. 12(2), 1\u201343 (2016)","journal-title":"Log. Methods Comput. Sci."},{"key":"395_CR8","doi-asserted-by":"crossref","unstructured":"Bocchi, L., Honda, K., Tuosto, E., Yoshida, N.: A theory of design-by-contract for distributed multiparty interactions. In: CONCUR 2010, volume 6269 of LNCS, pp. 162\u2013176. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-15375-4_12"},{"key":"395_CR9","doi-asserted-by":"crossref","unstructured":"Bocchi, L., Murgia, M., Vasconcelos, V.T., Yoshida, N.: Asynchronous timed session types - from duality to time-sensitive processes. In: Programming Languages and Systems\u201428th European Symposium on Programming, ESOP 2019, Prague, Czech Republic, Proceedings, pp. 583\u2013610 (2019)","DOI":"10.1007\/978-3-030-17184-1_21"},{"key":"395_CR10","doi-asserted-by":"crossref","unstructured":"Buscemi, M.G., Coppo, M., Dezani-Ciancaglini, M., Montanari, U.: Constraints for service contracts. In: Trustworthy Global Computing - 6th International Symposium, TGC 2011, Aachen, Germany, June 9\u201310, 2011. Revised Selected Papers, pp. 104\u2013120 (2011)","DOI":"10.1007\/978-3-642-30065-3_7"},{"key":"395_CR11","doi-asserted-by":"crossref","unstructured":"Buscemi, M.G., Melgratti, H.C.: Transactional service level agreement. In: Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5\u20136, 2007, Revised Selected Papers, pp. 124\u2013139 (2007)","DOI":"10.1007\/978-3-540-78663-4_10"},{"key":"395_CR12","doi-asserted-by":"crossref","unstructured":"Buscemi, M.G., Montanari, U.: Cc-pi: A constraint-based language for specifying service level agreements. In: ESOP 2007, volume 4421 of LNCS, pp. 18\u201332. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-71316-6_3"},{"key":"395_CR13","unstructured":"Buscemi, M.G., Montanari, U.: Open bisimulation for the concurrent constraint pi-calculus. In: Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29\u2013April 6, 2008. Proceedings, pp. 254\u2013268 (2008)"},{"key":"395_CR14","doi-asserted-by":"crossref","unstructured":"Buscemi, M.G., Montanari, U.: Cc-pi: A constraint language for service negotiation and composition. In: Results of the SENSORIA Project, volume 6582 of LNCS, pp. 262\u2013281. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-20401-2_12"},{"key":"395_CR15","unstructured":"Cano, M.: Session-Based Concurrency: Between Operational and Declarative Views. Ph.D. thesis, University of Groningen (2020)"},{"key":"395_CR16","unstructured":"Cano, M., Arias, J., P\u00e9rez, J.A.: Session-based concurrency, reactively. In: Bouajjani, A., Silva, A. (eds.) Formal Techniques for Distributed Objects, Components, and Systems\u201437th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuch\u00e2tel, Switzerland, June 19\u201322, 2017, Proceedings, volume 10321 of Lecture Notes in Computer Science, pp. 74\u201391. Springer, Berlin (2017)"},{"key":"395_CR17","doi-asserted-by":"crossref","unstructured":"Cano, M., Rueda, C., L\u00f3pez, H.A., P\u00e9rez, J.A.: Declarative interpretations of session-based concurrency. In: Proceedings of the International Symposium on Principles and Practice of Declarative Programming (PPDP) 2015, pp. 67\u201378. ACM (2015)","DOI":"10.1145\/2790449.2790513"},{"key":"395_CR18","first-page":"29","volume":"2010","author":"M Carbone","year":"2010","unstructured":"Carbone, M., Grohmann, D., Hildebrandt, T.T., L\u00f3pez, H.A.: A logic for choreographies. Proc. Places 2010, 29\u201343 (2010)","journal-title":"Proc. Places"},{"key":"395_CR19","doi-asserted-by":"crossref","unstructured":"Colombo, C., Pace, G.J., Schneider, G.: LARVA\u2014safer monitoring of real-time java programs (tool paper). In: Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, Hanoi, Vietnam, 23\u201327 November 2009, pp. 33\u201337 (2009)","DOI":"10.1109\/SEFM.2009.13"},{"key":"395_CR20","doi-asserted-by":"crossref","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: Structured communications with concurrent constraints. In: Proceedings of TGC 2008, volume 5474 of LNCS, pp. 104\u2013125. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-00945-7_7"},{"issue":"2","key":"395_CR21","doi-asserted-by":"publisher","first-page":"291","DOI":"10.19153\/cleiej.1.2.2","volume":"1","author":"JF D\u00edaz","year":"1998","unstructured":"D\u00edaz, J.F., Rueda, C., Valencia, F.D.: Pi+- calculus: a calculus for concurrent processes with constraints. CLEI Electron. J. 1(2), 291 (1998)","journal-title":"CLEI Electron. J."},{"issue":"1","key":"395_CR22","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1006\/inco.2000.3002","volume":"165","author":"F Fages","year":"2001","unstructured":"Fages, F., Ruet, P., Soliman, S.: Linear concurrent constraint programming: Operational and phase semantics. Inf. Comput. 165(1), 14\u201341 (2001)","journal-title":"Inf. Comput."},{"key":"395_CR23","doi-asserted-by":"crossref","unstructured":"Gay, S.J., Thiemann, P., Vasconcelos, V.T.: Duality of session types: The final cut. In: Balzer, S., Padovani, L. (eds.) Proceedings of the 12th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES@ETAPS 2020, Dublin, Ireland, 26th April 2020, volume 314 of EPTCS, pp. 23\u201333 (2020)","DOI":"10.4204\/EPTCS.314.0"},{"key":"395_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J-Y Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1\u2013102 (1987)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"395_CR25","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/s00446-010-0120-6","volume":"23","author":"D Gorla","year":"2010","unstructured":"Gorla, D.: A taxonomy of process calculi for distribution and mobility. Distrib. Comput. 23(4), 273\u2013299 (2010)","journal-title":"Distrib. Comput."},{"issue":"9","key":"395_CR26","doi-asserted-by":"publisher","first-page":"1031","DOI":"10.1016\/j.ic.2010.05.002","volume":"208","author":"D Gorla","year":"2010","unstructured":"Gorla, D.: Towards a unified approach to encodability and separation results for process calculi. Inf. Comput. 208(9), 1031\u20131053 (2010)","journal-title":"Inf. Comput."},{"issue":"4\u20135","key":"395_CR27","first-page":"469","volume":"11","author":"R Haemmerl\u00e9","year":"2011","unstructured":"Haemmerl\u00e9, R.: Observational equivalences for linear logic concurrent constraint languages. TPLP 11(4\u20135), 469\u2013485 (2011)","journal-title":"TPLP"},{"key":"395_CR28","doi-asserted-by":"crossref","unstructured":"Hildebrandt, T.T., L\u00f3pez, H.A.: Types for secure pattern matching with local knowledge in universal concurrent constraint programming. In: Logic Programming, 25th International Conference, ICLP 2009, Pasadena, CA, USA, July 14-17, 2009. Proceedings, pp. 417\u2013431 (2009)","DOI":"10.1007\/978-3-642-02846-5_34"},{"key":"395_CR29","doi-asserted-by":"crossref","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language Primitives and Type Discipline for Structured Communication-Based Programming. In: Proceedings of ESOP\u201998, vol. 1381, pp. 122\u2013138. Springer, Berlin (1998)","DOI":"10.1007\/BFb0053567"},{"key":"395_CR30","doi-asserted-by":"crossref","unstructured":"Klensin, J.: Simple mail transfer protocol. https:\/\/tools.ietf.org\/html\/rfc5321. Accessed July, 2019 (2008)","DOI":"10.17487\/rfc5321"},{"key":"395_CR31","doi-asserted-by":"crossref","unstructured":"L\u00f3pez, H.A., Olarte, C., P\u00e9rez, J.A.: Towards a unified framework for declarative structured communications. In: PLACES 2009, York, UK, 22nd March 2009, volume\u00a017 of EPTCS, pp. 1\u201315 (2009)","DOI":"10.4204\/EPTCS.17.1"},{"key":"395_CR32","doi-asserted-by":"crossref","unstructured":"Mandel, L., Pouzet, M.: ReactiveML: a reactive extension to ML. In: Proceedings of PPDP\u201905, pp. 82\u201393. ACM (2005)","DOI":"10.1145\/1069774.1069782"},{"issue":"1","key":"395_CR33","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. I. Inf. Comput. 100(1), 1\u201340 (1992)","journal-title":"Inf. Comput."},{"issue":"1","key":"395_CR34","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/0890-5401(92)90009-5","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. II. Inf. Comput. 100(1), 41\u201377 (1992)","journal-title":"Inf. Comput."},{"key":"395_CR35","doi-asserted-by":"crossref","unstructured":"Monjaraz, R., Mari\u00f1o, J.: From the $$\\pi $$-calculus to flat GHC. In: Proceedings of PPDP\u201912, pp. 163\u2013172. ACM (2012)","DOI":"10.1145\/2370776.2370797"},{"issue":"5","key":"395_CR36","doi-asserted-by":"publisher","first-page":"877","DOI":"10.1007\/s00165-017-0420-8","volume":"29","author":"R Neykova","year":"2017","unstructured":"Neykova, R., Bocchi, L., Yoshida, N.: Timed runtime monitoring for multiparty conversations. Formal Asp. Comput. 29(5), 877\u2013910 (2017)","journal-title":"Formal Asp. Comput."},{"key":"395_CR37","doi-asserted-by":"crossref","unstructured":"Olarte, C., Valencia, F.D.: Universal concurrent constraint programing: symbolic semantics and applications to security. In: Proceedings of the 2008 ACM Symposium on Applied Computing (SAC), Fortaleza, Ceara, Brazil, March 16-20, 2008, pp. 145\u2013150 (2008)","DOI":"10.1145\/1363686.1363726"},{"key":"395_CR38","doi-asserted-by":"crossref","unstructured":"Parrow, J.: Trios in concert. In: Proof, Language, and Interaction, Essays in Honour of Robin Milner, pp. 623\u2013638 (2000)","DOI":"10.7551\/mitpress\/5641.003.0030"},{"key":"395_CR39","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/j.entcs.2008.04.011","volume":"209","author":"J Parrow","year":"2008","unstructured":"Parrow, J.: Expressiveness of process algebras. Electr. Notes Theor. Comput. Sci. 209, 173\u2013186 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"395_CR40","doi-asserted-by":"crossref","unstructured":"Peters, K.: Comparing process calculi using encodings. In: P\u00e9rez, J.A., Rot, J. (eds). Proceedings Combined 26th International Workshop on Expressiveness in Concurrency and 16th Workshop on Structural Operational Semantics, EXPRESS\/SOS 2019, Amsterdam, The Netherlands, 26th August 2019, volume 300 of EPTCS, pp. 19\u201338 (2019)","DOI":"10.4204\/EPTCS.300.0"},{"key":"395_CR41","unstructured":"Peters, K., Nestmann, U.: Is it a \u201cgood\u201d encoding of mixed choice? In: Foundations of Software Science and Computational Structures\u201415th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24\u2013April 1, 2012. Proceedings, pp. 210\u2013224 (2012)"},{"key":"395_CR42","volume-title":"Types and Programming Languages","author":"BC Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"395_CR43","doi-asserted-by":"crossref","unstructured":"Saraswat, V.A.: Concurrent Constraint Programming. ACM Doctoral dissertation awards. MIT Press, Cambridge (1993)","DOI":"10.7551\/mitpress\/2086.001.0001"},{"key":"395_CR44","unstructured":"Soliman, S.: Pi-calcul et lcc, une odyss\u00e9e de l\u2019espace. In: Programmation en logique avec contraintes, JFPLC 2004, June 21\u201323 2004, Angers, France (2004)"},{"key":"395_CR45","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.ic.2012.05.002","volume":"217","author":"VT Vasconcelos","year":"2012","unstructured":"Vasconcelos, V.T.: Fundamentals of session types. Inf. Comput. 217, 52\u201370 (2012)","journal-title":"Inf. Comput."},{"key":"395_CR46","doi-asserted-by":"crossref","unstructured":"Yoshida, N., Hu, R., Neykova, R., Ng, N.: The scribble protocol language. In: TGC 2013, Buenos Aires, Argentina, August 30\u201331, 2013, Revised Selected Papers, pp. 22\u201341 (2013)","DOI":"10.1007\/978-3-319-14128-2_3"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-021-00395-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-021-00395-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-021-00395-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,26]],"date-time":"2024-08-26T08:48:58Z","timestamp":1724662138000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-021-00395-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,3,18]]},"references-count":46,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,2]]}},"alternative-id":["395"],"URL":"https:\/\/doi.org\/10.1007\/s00236-021-00395-w","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2021,3,18]]},"assertion":[{"value":"20 January 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 January 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 March 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}