{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,29]],"date-time":"2024-03-29T18:28:02Z","timestamp":1711736882228},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2018,7,30]],"date-time":"2018-07-30T00:00:00Z","timestamp":1532908800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,7,30]]},"abstract":"\n We study the problem of parametric parallel complexity analysis of concurrent, message-passing programs. To make the analysis local and compositional, it is based on a conservative extension of binary session types, which structure the type and direction of communication between processes and stand in a Curry-Howard correspondence with intuitionistic linear logic. The main innovation is to enrich session types with the\n temporal modalities<\/jats:italic>\n next<\/jats:italic>\n (\u25ef\n A<\/jats:italic>\n ),\n always<\/jats:italic>\n (\u25a1\n A<\/jats:italic>\n ), and\n eventually<\/jats:italic>\n (\u25c7\n A<\/jats:italic>\n ), to additionally prescribe the timing of the exchanged messages in a way that is precise yet flexible. The resulting\n temporal session types<\/jats:italic>\n uniformly express properties such as the message rate of a stream, the latency of a pipeline, the response time of a concurrent queue, or the span of a fork\/join parallel program. The analysis is parametric in the cost model and the presentation focuses on communication cost as a concrete example. The soundness of the analysis is established by proofs of progress and type preservation using a timed multiset rewriting semantics. Representative examples illustrate the scope and usability of the approach.\n <\/jats:p>","DOI":"10.1145\/3236786","type":"journal-article","created":{"date-parts":[[2018,7,31]],"date-time":"2018-07-31T19:41:18Z","timestamp":1533066078000},"page":"1-30","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Parallel complexity analysis with temporal session types"],"prefix":"10.1145","volume":"2","author":[{"given":"Ankush","family":"Das","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"given":"Jan","family":"Hoffmann","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]}],"member":"320","published-online":{"date-parts":[[2018,7,30]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Einar Broch Johnsen, and Guillermo Rom\u00e1n-D\u00edez","author":"Albert Elvira","year":"2015","unstructured":"Elvira Albert , Jes\u00fas Correas , Einar Broch Johnsen, and Guillermo Rom\u00e1n-D\u00edez . 2015 . Parallel Cost Analysis of Distributed Systems. In Static Analysis, Sandrine Blazy and Thomas Jensen (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg, 275\u2013292. Elvira Albert, Jes\u00fas Correas, Einar Broch Johnsen, and Guillermo Rom\u00e1n-D\u00edez. 2015. Parallel Cost Analysis of Distributed Systems. In Static Analysis, Sandrine Blazy and Thomas Jensen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 275\u2013292."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784753"},{"key":"e_1_2_2_3_1","volume-title":"Manifest Sharing with Session Types. In International Conference on Functional Programming (ICFP). ACM, 37:1\u201337:29","author":"Balzer Stephanie","year":"2017","unstructured":"Stephanie Balzer and Frank Pfenning . 2017 . Manifest Sharing with Session Types. In International Conference on Functional Programming (ICFP). ACM, 37:1\u201337:29 . Stephanie Balzer and Frank Pfenning. 2017. Manifest Sharing with Session Types. In International Conference on Functional Programming (ICFP). ACM, 37:1\u201337:29."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/258492.258517"},{"key":"e_1_2_2_6_1","volume-title":"Timed Multiparty Session Types. In CONCUR 2014 \u2013 Concurrency Theory, Paolo Baldan and Daniele Gorla (Eds.). Springer Berlin Heidelberg","author":"Bocchi Laura","year":"2014","unstructured":"Laura Bocchi , Weizhen Yang , and Nobuko Yoshida . 2014 . Timed Multiparty Session Types. In CONCUR 2014 \u2013 Concurrency Theory, Paolo Baldan and Daniele Gorla (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg, 419\u2013434. Laura Bocchi, Weizhen Yang, and Nobuko Yoshida. 2014. Timed Multiparty Session Types. In CONCUR 2014 \u2013 Concurrency Theory, Paolo Baldan and Daniele Gorla (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 419\u2013434."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_19"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887654.1887670"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000218"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.11.006"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784749"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209146"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788825"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_11"},{"key":"e_1_2_2_15_1","volume-title":"Cuts for Circular Proofs: Semantics and Cut Elimination. In 22nd Conference on Computer Science Logic (LIPIcs)","volume":"23","author":"Fortier J\u00e9r\u00f4me","year":"2013","unstructured":"J\u00e9r\u00f4me Fortier and Luigi Santocanale . 2013 . Cuts for Circular Proofs: Semantics and Cut Elimination. In 22nd Conference on Computer Science Logic (LIPIcs) , Vol. 23 . 248\u2013262. J\u00e9r\u00f4me Fortier and Luigi Santocanale. 2013. Cuts for Circular Proofs: Semantics and Cut Elimination. In 22nd Conference on Computer Science Logic (LIPIcs), Vol. 23. 248\u2013262."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837646"},{"key":"e_1_2_2_20_1","volume-title":"Gunter","author":"Griffith Dennis","year":"2013","unstructured":"Dennis Griffith and Elsa L . Gunter . 2013 . Liquid Pi : Inferrable Dependent Session Types. In Proceedings of the NASA Formal Methods Symposium. Springer LNCS 7871, 186\u2013197. Dennis Griffith and Elsa L. Gunter. 2013. Liquid Pi: Inferrable Dependent Session Types. In Proceedings of the NASA Formal Methods Symposium. Springer LNCS 7871, 186\u2013197."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480898"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/4472.4478"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_6"},{"key":"e_1_2_2_26_1","volume-title":"Language Primitives and Type Discipline for Structured Communication-Based Programming. In 7th European Symposium on Programming Languages and Systems (ESOP\u201998)","author":"Honda Kohei","year":"1998","unstructured":"Kohei Honda , Vasco T. Vasconcelos , and Makoto Kubo . 1998 . Language Primitives and Type Discipline for Structured Communication-Based Programming. In 7th European Symposium on Programming Languages and Systems (ESOP\u201998) . Springer LNCS 1381, 122\u2013138. Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In 7th European Symposium on Programming Languages and Systems (ESOP\u201998). Springer LNCS 1381, 122\u2013138."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(02)93171-8"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.38"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.22"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_26"},{"key":"e_1_2_2_31_1","volume-title":"Proceedings of the Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software (PLACES), A. Beresford and S. Gay (Eds.). EPTCS 17","author":"L\u00f3pez Hugo A.","unstructured":"Hugo A. L\u00f3pez , Carlos Olarte , and Jorge A. P\u00e9rez . 2009. Towards a Unified Framework for Declarative Structure Communications . In Proceedings of the Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software (PLACES), A. Beresford and S. Gay (Eds.). EPTCS 17 , 1\u201315. Hugo A. L\u00f3pez, Carlos Olarte, and Jorge A. P\u00e9rez. 2009. Towards a Unified Framework for Declarative Structure Communications. In Proceedings of the Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software (PLACES), A. Beresford and S. Gay (Eds.). EPTCS 17, 1\u201315."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/788022.789002"},{"key":"e_1_2_2_33_1","volume-title":"Timed Runtime Monitoring for Multiparty Conversations. In 3rd International Workshop on Behavioural Types (BEAT","author":"Neykova Rumyana","year":"2014","unstructured":"Rumyana Neykova , Laura Bocchi , and Nobuko Yoshida . 2014 . Timed Runtime Monitoring for Multiparty Conversations. In 3rd International Workshop on Behavioural Types (BEAT 2014). Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. 2014. Timed Runtime Monitoring for Multiparty Conversations. In 3rd International Workshop on Behavioural Types (BEAT 2014)."},{"key":"e_1_2_2_34_1","doi-asserted-by":"crossref","unstructured":"W. Paul U. Vishkin and H. Wagener. 1983. Parallel dictionaries on 2\u20133 trees. In Automata Languages and Programming Josep Diaz (Ed.). Springer Berlin Heidelberg Berlin Heidelberg 597\u2013609. W. Paul U. Vishkin and H. Wagener. 1983. Parallel dictionaries on 2\u20133 trees. In Automata Languages and Programming Josep Diaz (Ed.). Springer Berlin Heidelberg Berlin Heidelberg 597\u2013609.","DOI":"10.1007\/BFb0036940"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_1"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_2_37_1","unstructured":"Marc Pouzet. 2006. Lucid Synchrone Release version 3.0 Tutorial and Reference Manual. (2006). Marc Pouzet. 2006. Lucid Synchrone Release version 3.0 Tutorial and Reference Manual. (2006)."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-14128-2_8"},{"key":"e_1_2_2_39_1","volume-title":"Non-Blocking Concurrent Imperative Programming with Session Types. In Fourth International Workshop on Linearity.","author":"Silva Miguel","year":"2016","unstructured":"Miguel Silva , M\u00e1rio Florido , and Frank Pfenning . 2016 . Non-Blocking Concurrent Imperative Programming with Session Types. In Fourth International Workshop on Linearity. Miguel Silva, M\u00e1rio Florido, and Frank Pfenning. 2016. Non-Blocking Concurrent Imperative Programming with Session Types. In Fourth International Workshop on Linearity."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_20"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45917-1_11"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364568"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009858"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236786","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T19:47:00Z","timestamp":1672516020000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236786"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,30]]},"references-count":42,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2018,7,30]]}},"alternative-id":["10.1145\/3236786"],"URL":"https:\/\/doi.org\/10.1145\/3236786","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7,30]]},"assertion":[{"value":"2018-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}