{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T19:41:06Z","timestamp":1743018066346,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720186"},{"type":"electronic","value":"9783030720193"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Type systems as a technique to analyse or control programs have been extensively studied for functional programming languages. In particular some systems allow to extract from a typing derivation a complexity bound on the program. We explore how to extend such results to parallel complexity in the setting of the pi-calculus, considered as a communication-based model for parallel computation. Two notions of time complexity are given: the total computation time without parallelism (the work) and the computation time under maximal parallelism (the span). We define operational semantics to capture those two notions, and present two type systems from which one can extract a complexity bound on a process. The type systems are inspired both by size types and by input\/output types, with additional temporal information about communications.<\/jats:p>","DOI":"10.1007\/978-3-030-72019-3_3","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"59-86","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Types for Complexity of Parallel Computation in Pi-Calculus"],"prefix":"10.1007","author":[{"given":"Patrick","family":"Baillot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexis","family":"Ghyselen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Akl, S.G.: Encyclopedia of Parallel Computing, chap. Bitonic Sort, pp. 139\u2013146. Springer US, Boston, MA (2011)","DOI":"10.1007\/978-0-387-09766-4_124"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Albert, E., Correas, J., Johnsen, E.B., Rom\u00e1n-D\u00edez, G.: Parallel cost analysis of distributed systems. In: Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9291, pp. 275\u2013292. Springer (2015)","DOI":"10.1007\/978-3-662-48288-9_16"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Albert, E., Flores-Montoya, A., Genaim, S., Martin-Martin, E.: Rely-guarantee termination and cost analyses of loops with concurrent interleavings. Journal of Automated Reasoning 59(1), 47\u201385 (2017)","DOI":"10.1007\/s10817-016-9400-6"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Avanzini, M., Dal Lago, U.: Automating sized-type inference for complexity analysis. Proceedings of the ACM on Programming Languages 1(ICFP), 43 (2017)","DOI":"10.1145\/3110287"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Baillot, P., Ghyselen, A.: Types for Complexity of Parallel Computation in Pi-calculus (Technical Report) (Oct 2020), https:\/\/hal.archives-ouvertes.fr\/hal-02961427, working paper or preprint","DOI":"10.26226\/morressier.604907f41a80aac83ca25d13"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Dal Lago, U., Gaboardi, M.: Linear dependent types and relative completeness. In: Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on. pp. 133\u2013142. IEEE (2011)","DOI":"10.1109\/LICS.2011.22"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Dal Lago, U., Martini, S., Sangiorgi, D.: Light logics and higher-order processes. Mathematical Structures in Computer Science 26(6), 969\u2013992 (2016)","DOI":"10.1017\/S0960129514000310"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. Information and Computation 256, 253 \u2013 286 (2017)","DOI":"10.1016\/j.ic.2017.06.002"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Das, A., Hoffmann, J., Pfenning, F.: Parallel complexity analysis with temporal session types. Proc. ACM Program. Lang. 2(ICFP), 91:1\u201391:30 (2018).","DOI":"10.1145\/3236786"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Das, A., Hoffmann, J., Pfenning, F.: Work analysis with resource-aware session types. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 305\u2013314. ACM (2018).","DOI":"10.1145\/3209108.3209146"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Degano, P., Gadducci, F., Priami, C.: Causality and replication in concurrent processes. In: Perspectives of System Informatics. pp. 307\u2013318. Springer Berlin Heidelberg (2003)","DOI":"10.1007\/978-3-540-39866-0_30"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Degano, P., Priami, C.: Causality for mobile processes. In: Automata, Languages and Programming. pp. 660\u2013671. Springer Berlin Heidelberg (1995)","DOI":"10.1007\/3-540-60084-1_113"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Demangeon, R., Yoshida, N.: Causal computational complexity of distributed processes. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science. pp. 344\u2013353. LICS \u201918, ACM (2018)","DOI":"10.1145\/3209108.3209122"},{"key":"3_CR14","unstructured":"Di Giamberardino, P., Dal Lago, U.: On session types and polynomial time. Mathematical Structures in Computer Science -1 (2015)"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Gaboardi, M., Marion, J., Rocca, S.R.D.: A logical account of pspace. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008. pp. 121\u2013131. ACM (2008)","DOI":"10.1145\/1328897.1328456"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Giachino, E., Johnsen, E.B., Laneve, C., Pun, K.I.: Time complexity of concurrent programs - - A technique based on behavioural types -. In: Formal Aspects of Component Software - 12th International Conference, FACS 2015, Niter\u00f3i, Brazil, October 14-16, 2015, Revised Selected Papers. Lecture Notes in Computer Science, vol. 9539, pp. 199\u2013216. Springer (2016)","DOI":"10.1007\/978-3-319-28934-2_11"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Gimenez, S., Moser, G.: The complexity of interaction. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. pp. 243\u2013255 (2016)","DOI":"10.1145\/2837614.2837646"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Hainry, E., Marion, J.Y., P\u00e9choux, R.: Type-based complexity analysis for fork processes. In: Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7794, pp. 305\u2013320. Springer (2013)","DOI":"10.1007\/978-3-642-37075-5_20"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Harper, R.: Practical Foundations for Programming Languages. Cambridge University Press (2012)","DOI":"10.1017\/CBO9781139342131"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34(3), 14:1\u201314:62 (2012)","DOI":"10.1145\/2362389.2362393"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Resource aware ML. In: Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. Lecture Notes in Computer Science, vol. 7358, pp. 781\u2013786. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6012, pp. 287\u2013306. Springer (2010)","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Shao, Z.: Automatic static cost analysis for parallel programs. In: Vitek, J. (ed.) Programming Languages and Systems. pp. 132\u2013157. Springer Berlin Heidelberg, Berlin, Heidelberg (2015)","DOI":"10.1007\/978-3-662-46669-8_6"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: Linear types and non-size-increasing polynomial time computation. Information and Computation 183(1), 57\u201385 (2003)","DOI":"10.1016\/S0890-5401(03)00009-9"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, Louisisana, USA, January 15-17, 2003. pp. 185\u2013197. ACM (2003)","DOI":"10.1145\/604131.604148"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 410\u2013423. ACM (1996)","DOI":"10.1145\/237721.240882"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: A type system for lock-free processes. Information and Computation 177(2), 122 \u2013 159 (2002)","DOI":"10.1016\/S0890-5401(02)93171-8"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Type systems for concurrent programs. In: Formal Methods at the Crossroads. From Panacea to Foundational Support, pp. 439\u2013453. Springer (2003)","DOI":"10.1007\/978-3-540-40007-3_26"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Type-based information flow analysis for the $$\\pi $$-calculus. Acta Informatica 42(4-5), 291\u2013347 (2005)","DOI":"10.1007\/s00236-005-0179-x"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: A new type system for deadlock-free processes. In: International Conference on Concurrency Theory. pp. 233\u2013247. Springer (2006)","DOI":"10.1007\/11817949_16"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. 21(5), 914\u2013947 (sep 1999)","DOI":"10.1145\/330249.330251"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Madet, A., Amadio, R.M.: An elementary affine $$\\lambda $$-calculus with multithreading and side effects. In: Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6690, pp. 138\u2013152. Springer (2011)","DOI":"10.1007\/978-3-642-21691-6_13"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Marion, J.Y.: A type system for complexity flow analysis. In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada. pp. 123\u2013132. IEEE Computer Society (2011)","DOI":"10.1109\/LICS.2011.41"},{"key":"3_CR34","unstructured":"Sangiorgi, D., Walker, D.: The pi-calculus: a Theory of Mobile Processes. Cambridge University Press (2003)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72019-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T04:45:30Z","timestamp":1671684330000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-72019-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720186","9783030720193"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72019-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"79","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference took place virtually due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}