{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T19:50:46Z","timestamp":1771703446746,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":79,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3322484","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"502-516","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["Verifying message-passing programs with dependent behavioural types"],"prefix":"10.1145","author":[{"given":"Alceste","family":"Scalas","sequence":"first","affiliation":[{"name":"Imperial College London, UK \/ Aston University, UK"}]},{"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"Elias","family":"Benussi","sequence":"additional","affiliation":[{"name":"Imperial College London, UK \/ Faculty Science, UK"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"crossref","unstructured":"Umut A. Acar Arthur Chargueraud and Mike Rainey. 2013. Scheduling Parallel Programs by Work Stealing with Private Deques. In PPoPP.   Umut A. Acar Arthur Chargueraud and Mike Rainey. 2013. Scheduling Parallel Programs by Work Stealing with Private Deques. In PPoPP .","DOI":"10.1145\/2442516.2442538"},{"key":"e_1_3_2_2_2_1","volume-title":"A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday.","author":"Amin Nada","unstructured":"Nada Amin , Samuel Grutter , Martin Odersky , Tiark Rompf , and Sandro Stucki . 2016. The Essence of Dependent Object Types . In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. Nada Amin, Samuel Grutter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The Essence of Dependent Object Types. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday."},{"key":"e_1_3_2_2_3_1","volume-title":"Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida.","author":"Ancona Davide","year":"2017","unstructured":"Davide Ancona , Viviana Bono , Mario Bravetti , Joana Campos , Giuseppe Castagna , Pierre-Malo Denielou , Simon J. Gay , Nils Gesbert , Elena Giachino , Raymond Hu , Einar Broch Johnsen , Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. 2017 . Behavioral Types in Programming Languages. Foundations and Trends in Programming Languages 3(2-3) (2017). Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Denielou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. 2017. Behavioral Types in Programming Languages. Foundations and Trends in Programming Languages 3(2-3) (2017)."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110281"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/324133.324234"},{"key":"e_1_3_2_2_6_1","volume-title":"Handbook of Modal Logic","author":"Bradfield Julian","unstructured":"Julian Bradfield and Colin Stirling . 2007. Modal \u03bc-calculi . In Handbook of Modal Logic . Elsevier . Julian Bradfield and Colin Stirling. 2007. Modal \u03bc-calculi. In Handbook of Modal Logic. Elsevier."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950999017X"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"crossref","unstructured":"L. Cardelli S. Martini J.C. Mitchell and A. Scedrov. 1994. An Extension of System F with Subtyping. Information and Computation 109 1 (1994).   L. Cardelli S. Martini J.C. Mitchell and A. Scedrov. 1994. An Extension of System F with Subtyping. Information and Computation 109 1 (1994).","DOI":"10.1006\/inco.1994.1013"},{"key":"e_1_3_2_2_9_1","first-page":"53","article-title":"On Understanding Types, Data Abstraction, and","volume":"17","author":"Cardelli Luca","year":"1985","unstructured":"Luca Cardelli and Peter Wegner . 1985 . On Understanding Types, Data Abstraction, and Polymorphism. Comput. Surveys 17 , 4 (1985), 53 . Luca Cardelli and Peter Wegner. 1985. On Understanding Types, Data Abstraction, and Polymorphism. Comput. Surveys 17, 4 (1985), 53.","journal-title":"Polymorphism. Comput. Surveys"},{"key":"e_1_3_2_2_10_1","volume-title":"Proc. ACM Program. Lang. 3, POPL, Article 29","author":"Castro David","year":"2019","unstructured":"David Castro , Raymond Hu , Sung-Shik Jongmans , Nicholas Ng , and Nobuko Yoshida . 2019 . Distributed Programming Using Roleparametric Session Types in Go: Statically-typed Endpoint APIs for Dynamically-instantiated Communication Structures . Proc. ACM Program. Lang. 3, POPL, Article 29 (2019). David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. 2019. Distributed Programming Using Roleparametric Session Types in Go: Statically-typed Endpoint APIs for Dynamically-instantiated Communication Structures. Proc. ACM Program. Lang. 3, POPL, Article 29 (2019)."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Mario Coppo Mariangiola Dezani-Ciancaglini Luca Padovani and Nobuko Yoshida. 2015. A Gentle Introduction to Multiparty Asynchronous Session Types. In Formal Methods for Multicore Programming.  Mario Coppo Mariangiola Dezani-Ciancaglini Luca Padovani and Nobuko Yoshida. 2015. A Gentle Introduction to Multiparty Asynchronous Session Types. In Formal Methods for Multicore Programming .","DOI":"10.1007\/978-3-319-18941-3_4"},{"key":"e_1_3_2_2_12_1","volume-title":"Global Progress for Dynamically Interleaved Multiparty Sessions. MSCS 760","author":"Coppo Mario","year":"2015","unstructured":"Mario Coppo , Mariangiola Dezani-Ciancaglini , Nobuko Yoshida , and Luca Padovani . 2015. Global Progress for Dynamically Interleaved Multiparty Sessions. MSCS 760 ( 2015 ). Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. 2015. Global Progress for Dynamically Interleaved Multiparty Sessions. MSCS 760 (2015)."},{"key":"e_1_3_2_2_13_1","unstructured":"Ugo de'Liguoro and Luca Padovani. 2018. Mailbox Types for Unordered Interactions. In ECOOP.  Ugo de'Liguoro and Luca Padovani. 2018. Mailbox Types for Unordered Interactions. In ECOOP ."},{"key":"e_1_3_2_2_14_1","volume-title":"Parameterised Multiparty Session Types. Logical Methods in Computer Science 8, 4","author":"Denielou Pierre-Malo","year":"2012","unstructured":"Pierre-Malo Denielou , Nobuko Yoshida , Andi Bejleri , and Raymond Hu. 2012. Parameterised Multiparty Session Types. Logical Methods in Computer Science 8, 4 ( 2012 ). Pierre-Malo Denielou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. 2012. Parameterised Multiparty Session Types. Logical Methods in Computer Science 8, 4 (2012)."},{"key":"e_1_3_2_2_15_1","volume-title":"Static Analysis.","author":"D'Osualdo Emanuele","unstructured":"Emanuele D'Osualdo , Jonathan Kochems , and C. H. Luke Ong . 2013. Automatic Verification of Erlang-Style Concurrency . In Static Analysis. Berlin, Heidelberg . Emanuele D'Osualdo, Jonathan Kochems, and C. H. Luke Ong. 2013. Automatic Verification of Erlang-Style Concurrency. In Static Analysis. Berlin, Heidelberg."},{"key":"e_1_3_2_2_16_1","unstructured":"Dotty developers. 2019. Dotty documentation: dependent function types. https:\/\/dotty.epfl.ch\/docs\/reference\/new-types\/dependent-function-types.html.  Dotty developers. 2019. Dotty documentation: dependent function types. https:\/\/dotty.epfl.ch\/docs\/reference\/new-types\/dependent-function-types.html."},{"key":"e_1_3_2_2_17_1","unstructured":"Dotty developers. 2019. Dotty documentation: match types. http:\/\/dotty.epfl.ch\/docs\/reference\/new-types\/match-types.html.  Dotty developers. 2019. Dotty documentation: match types. http:\/\/dotty.epfl.ch\/docs\/reference\/new-types\/match-types.html."},{"key":"e_1_3_2_2_18_1","unstructured":"Ericsson. 2019. The Erlang\/OTP Programming Language and Toolkit. http:\/\/erlang.org\/.  Ericsson. 2019. The Erlang\/OTP Programming Language and Toolkit. http:\/\/erlang.org\/."},{"key":"e_1_3_2_2_19_1","unstructured":"Javier Esparza. 1994. On the decidability of model checking for several \u03bc-calculi and Petri nets. In Trees in Algebra and Programming D CAAP.   Javier Esparza. 1994. On the decidability of model checking for several \u03bc-calculi and Petri nets. In Trees in Algebra and Programming D CAAP ."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050074"},{"key":"e_1_3_2_2_21_1","volume-title":"Article 7","author":"Giesl Jurgen","year":"2011","unstructured":"Jurgen Giesl , Matthias Raffelsieper , Peter Schneider-Kamp , Stephan Swiderski , and Rene Thiemann . 2011. Automated Termination Proofs for Haskell by Term Rewriting. TOPLAS 33, 2 , Article 7 ( 2011 ). Jurgen Giesl, Matthias Raffelsieper, Peter Schneider-Kamp, Stephan Swiderski, and Rene Thiemann. 2011. Automated Termination Proofs for Haskell by Term Rewriting. TOPLAS 33, 2, Article 7 (2011)."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Ursula Goltz. 1990. CCS and Petri nets. In Semantics of Systems of Concurrent Processes.   Ursula Goltz. 1990. CCS and Petri nets. In Semantics of Systems of Concurrent Processes .","DOI":"10.1007\/3-540-53479-2_14"},{"key":"e_1_3_2_2_23_1","volume-title":"Modeling and Analysis of Communicating Systems","author":"Groote Jan Friso","unstructured":"Jan Friso Groote and Mohammad Reza Mousavi . 2014. Modeling and Analysis of Communicating Systems . The MIT Press . Jan Friso Groote and Mohammad Reza Mousavi. 2014. Modeling and Analysis of Communicating Systems. The MIT Press."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2697431.2697623"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"crossref","unstructured":"Carl Hewitt Peter Bishop Irene Greif Brian Smith Todd Matson and Richard Steiger. 1973. Actor Induction and Meta-evaluation. In POPL.   Carl Hewitt Peter Bishop Irene Greif Brian Smith Todd Matson and Richard Steiger. 1973. Actor Induction and Meta-evaluation. In POPL .","DOI":"10.1145\/512927.512942"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"crossref","unstructured":"Kohei Honda. 1993. Types for Dyadic Interaction. In CONCUR.  Kohei Honda. 1993. Types for Dyadic Interaction. In CONCUR .","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_3_2_2_27_1","article-title":"Multiparty asynchronous session types. In POPL","author":"Honda Kohei","year":"2008","unstructured":"Kohei Honda , Nobuko Yoshida , and Marco Carbone . 2008 . Multiparty asynchronous session types. In POPL . Journal version in [28]. Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty asynchronous session types. In POPL. Journal version in [28].","journal-title":"Journal version in [28]."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"crossref","unstructured":"Atsushi Igarashi and Naoki Kobayashi. 2001. A Generic Type System for the Pi-calculus. In POPL.   Atsushi Igarashi and Naoki Kobayashi. 2001. A Generic Type System for the Pi-calculus. In POPL .","DOI":"10.1145\/360204.360215"},{"key":"e_1_3_2_2_30_1","volume-title":"A generic type system for the ?-calculus. TCS 311, 1","author":"Igarashi Atsushi","year":"2004","unstructured":"Atsushi Igarashi and Naoki Kobayashi . 2004. A generic type system for the ?-calculus. TCS 311, 1 ( 2004 ). Atsushi Igarashi and Naoki Kobayashi. 2004. A generic type system for the ?-calculus. TCS 311, 1 (2004)."},{"key":"e_1_3_2_2_31_1","volume-title":"Imam and Vivek Sarkar","author":"Shams","year":"2014","unstructured":"Shams M. Imam and Vivek Sarkar . 2014 . Savina D An Actor Benchmark Suite: Enabling Empirical Evaluation of Actor Libraries (AGERE !). Shams M. Imam and Vivek Sarkar. 2014. Savina D An Actor Benchmark Suite: Enabling Empirical Evaluation of Actor Libraries (AGERE!)."},{"key":"e_1_3_2_2_32_1","unstructured":"Alan Jeffrey. 2001. A Symbolic Labelled Transition System for Coinductive Subtyping of F\u03bc>Types. In LICS.   Alan Jeffrey. 2001. A Symbolic Labelled Transition System for Coinductive Subtyping of F \u03bc>Types. In LICS ."},{"key":"e_1_3_2_2_33_1","unstructured":"Alexander Kaiser Daniel Kroening and Thomas Wahl. 2015. Bfc - A Widening Approach to Multi-Threaded Program Verification. http:\/\/www.cprover.org\/bfc\/.  Alexander Kaiser Daniel Kroening and Thomas Wahl. 2015. Bfc - A Widening Approach to Multi-Threaded Program Verification. http:\/\/www.cprover.org\/bfc\/."},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/AICCSA.2003.1227495"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"crossref","unstructured":"Gijs Kant Alfons Laarman Jeroen Meijer Jaco van de Pol Stefan Blom and Tom van Dijk. 2015. LTSmin: High-Performance Language-Independent Model Checking. In TACAS.   Gijs Kant Alfons Laarman Jeroen Meijer Jaco van de Pol Stefan Blom and Tom van Dijk. 2015. LTSmin: High-Performance Language-Independent Model Checking. In TACAS .","DOI":"10.1007\/978-3-662-46681-0_61"},{"key":"e_1_3_2_2_36_1","volume-title":"A Partially Deadlock-Free Typed Process Calculus. TOPLAS 20, 2","author":"Kobayashi Naoki","year":"1998","unstructured":"Naoki Kobayashi . 1998. A Partially Deadlock-Free Typed Process Calculus. TOPLAS 20, 2 ( 1998 ). Naoki Kobayashi. 1998. A Partially Deadlock-Free Typed Process Calculus. TOPLAS 20, 2 (1998)."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"crossref","unstructured":"Naoki Kobayashi. 2006. A New Type System for Deadlock-Free Processes. In CONCUR.   Naoki Kobayashi. 2006. A New Type System for Deadlock-Free Processes. In CONCUR .","DOI":"10.1007\/11817949_16"},{"key":"e_1_3_2_2_38_1","volume-title":"Deadlock analysis of unbounded process networks. Information and Computation 252","author":"Kobayashi Naoki","year":"2017","unstructured":"Naoki Kobayashi and Cosimo Laneve . 2017. Deadlock analysis of unbounded process networks. Information and Computation 252 ( 2017 ). Naoki Kobayashi and Cosimo Laneve. 2017. Deadlock analysis of unbounded process networks. Information and Computation 252 (2017)."},{"key":"e_1_3_2_2_39_1","volume-title":"A hybrid type system for lock-freedom of mobile processes. TOPLAS 32, 5","author":"Kobayashi Naoki","year":"2010","unstructured":"Naoki Kobayashi and Davide Sangiorgi . 2010. A hybrid type system for lock-freedom of mobile processes. TOPLAS 32, 5 ( 2010 ). Naoki Kobayashi and Davide Sangiorgi. 2010. A hybrid type system for lock-freedom of mobile processes. TOPLAS 32, 5 (2010)."},{"key":"e_1_3_2_2_40_1","volume-title":"Aneris: A Logic for Node-Local, Modular Reasoning of Distributed Systems. https:\/\/iris-project.org\/pdfs\/2019-aneris-submission.pdf. Unpublished draft.","author":"Krogh-Jespersen Morten","year":"2018","unstructured":"Morten Krogh-Jespersen , Amin Timany , and Lars Birkedal Marit Edna Ohlenbusch . 2018 . Aneris: A Logic for Node-Local, Modular Reasoning of Distributed Systems. https:\/\/iris-project.org\/pdfs\/2019-aneris-submission.pdf. Unpublished draft. Morten Krogh-Jespersen, Amin Timany, and Lars Birkedal Marit Edna Ohlenbusch. 2018. Aneris: A Logic for Node-Local, Modular Reasoning of Distributed Systems. https:\/\/iris-project.org\/pdfs\/2019-aneris-submission.pdf. Unpublished draft."},{"key":"e_1_3_2_2_41_1","unstructured":"Roland Kuhn. 2017. Akka Typed Session. https:\/\/github.com\/rkuhn\/akka-typed-session.  Roland Kuhn. 2017. Akka Typed Session. https:\/\/github.com\/rkuhn\/akka-typed-session."},{"key":"e_1_3_2_2_42_1","unstructured":"Roland Kuhn. 2017. Akka Typed Session: audit example. https:\/\/github.com\/rkuhn\/akka-typed-session\/blob\/master\/src\/test\/scala\/com\/rolandkuhn\/akka_typed_session\/auditdemo\/ProcessBased.scala.  Roland Kuhn. 2017. Akka Typed Session: audit example. https:\/\/github.com\/rkuhn\/akka-typed-session\/blob\/master\/src\/test\/scala\/com\/rolandkuhn\/akka_typed_session\/auditdemo\/ProcessBased.scala."},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"crossref","unstructured":"Julien Lange Nicholas Ng Bernardo Toninho and Nobuko Yoshida. 2017. Fencing off go: liveness and safety for channel-based programming. In POPL.   Julien Lange Nicholas Ng Bernardo Toninho and Nobuko Yoshida. 2017. Fencing off go: liveness and safety for channel-based programming. In POPL .","DOI":"10.1145\/3009837.3009847"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"crossref","unstructured":"Julien Lange Nicholas Ng Bernardo Toninho and Nobuko Yoshida. 2018. A static verification framework for message passing in Go using behavioural types. In ICSE.   Julien Lange Nicholas Ng Bernardo Toninho and Nobuko Yoshida. 2018. A static verification framework for message passing in Go using behavioural types. In ICSE .","DOI":"10.1145\/3180155.3180157"},{"key":"e_1_3_2_2_46_1","volume-title":"Akka Typed: Protocols. https:\/\/akka.io\/blog\/2017\/05\/12\/typed-protocols.","author":"Lightbend","year":"2017","unstructured":"Lightbend , Inc . 2017 . Akka Typed: Protocols. https:\/\/akka.io\/blog\/2017\/05\/12\/typed-protocols. Lightbend, Inc. 2017. Akka Typed: Protocols. https:\/\/akka.io\/blog\/2017\/05\/12\/typed-protocols."},{"key":"e_1_3_2_2_47_1","unstructured":"Lightbend Inc. 2019. Akka Dispatchers documentation. https:\/\/doc.akka.io\/docs\/akka\/2.5\/dispatchers.html.  Lightbend Inc. 2019. Akka Dispatchers documentation. https:\/\/doc.akka.io\/docs\/akka\/2.5\/dispatchers.html."},{"key":"e_1_3_2_2_48_1","unstructured":"Lightbend Inc. 2019. Akka remoting documentation. https:\/\/doc.akka.io\/docs\/akka\/2.5\/remoting.html.  Lightbend Inc. 2019. Akka remoting documentation. https:\/\/doc.akka.io\/docs\/akka\/2.5\/remoting.html."},{"key":"e_1_3_2_2_49_1","unstructured":"Lightbend Inc. 2019. The Akka toolkit and runtime. http:\/\/akka.io\/.  Lightbend Inc. 2019. The Akka toolkit and runtime. http:\/\/akka.io\/."},{"key":"e_1_3_2_2_50_1","unstructured":"Lightbend Inc. 2019. Akka Typed documentation. https:\/\/doc.akka.io\/docs\/akka\/2.5\/typed\/index.html.  Lightbend Inc. 2019. Akka Typed documentation. https:\/\/doc.akka.io\/docs\/akka\/2.5\/typed\/index.html."},{"key":"e_1_3_2_2_51_1","volume-title":"Wing","author":"Liskov Barbara H.","year":"1994","unstructured":"Barbara H. Liskov and Jeannette M . Wing . 1994 . A Behavioral Notion of Subtyping. TOPLAS 16, 6 (1994). Barbara H. Liskov and Jeannette M. Wing. 1994. A Behavioral Notion of Subtyping. TOPLAS 16, 6 (1994)."},{"key":"e_1_3_2_2_52_1","volume-title":"Spores: A Type-Based Foundation for Closures in the Age of Concurrency and Distribution. In ECOOP.","author":"Miller Heather","year":"2014","unstructured":"Heather Miller , Philipp Haller , and Martin Odersky . 2014 . Spores: A Type-Based Foundation for Closures in the Age of Concurrency and Distribution. In ECOOP. Heather Miller, Philipp Haller, and Martin Odersky. 2014. Spores: A Type-Based Foundation for Closures in the Age of Concurrency and Distribution. In ECOOP."},{"key":"e_1_3_2_2_53_1","volume-title":"Communication and Concurrency","author":"Milner Robin","unstructured":"Robin Milner . 1989. Communication and Concurrency . Prentice-Hall, Inc. Robin Milner. 1989. Communication and Concurrency. Prentice-Hall, Inc."},{"key":"e_1_3_2_2_54_1","volume-title":"Communicating and Mobile Systems: the ?-Calculus","author":"Milner Robin","unstructured":"Robin Milner . 1999. Communicating and Mobile Systems: the ?-Calculus . Cambridge University Press . Robin Milner. 1999. Communicating and Mobile Systems: the ?-Calculus. Cambridge University Press."},{"key":"e_1_3_2_2_55_1","volume-title":"Parts I and II. Information and Computation 100, 1","author":"Milner Robin","year":"1992","unstructured":"Robin Milner , Joachim Parrow , and David Walker . 1992. A Calculus of Mobile Processes , Parts I and II. Information and Computation 100, 1 ( 1992 ). Robin Milner, Joachim Parrow, and David Walker. 1992. A Calculus of Mobile Processes, Parts I and II. Information and Computation 100, 1 (1992)."},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"crossref","unstructured":"Hanne Riis Nielson and Flemming Nielson. 1994. Higher-order Concurrent Programs with Finite Communication Topology (Extended Abstract). In POPL.   Hanne Riis Nielson and Flemming Nielson. 1994. Higher-order Concurrent Programs with Finite Communication Topology (Extended Abstract). In POPL .","DOI":"10.1145\/174675.174538"},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158130"},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"crossref","unstructured":"Luca Padovani. 2014. Deadlock and lock freedom in the linear ? - calculus. In CSL-LICS.   Luca Padovani. 2014. Deadlock and lock freedom in the linear ? - calculus. In CSL-LICS .","DOI":"10.1145\/2603088.2603116"},{"key":"e_1_3_2_2_59_1","volume-title":"Miniphases: Compilation Using Modular and Efficient Tree Transformations. In PLDI.","author":"Petrashko Dmitry","year":"2017","unstructured":"Dmitry Petrashko , Ondrej Lhotak , and Martin Odersky . 2017 . Miniphases: Compilation Using Modular and Efficient Tree Transformations. In PLDI. Dmitry Petrashko, Ondrej Lhotak, and Martin Odersky. 2017. Miniphases: Compilation Using Modular and Efficient Tree Transformations. In PLDI."},{"key":"e_1_3_2_2_60_1","volume-title":"Types and programming languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce . 2002. Types and programming languages . MIT Press . Benjamin C. Pierce. 2002. Types and programming languages. MIT Press."},{"key":"e_1_3_2_2_61_1","volume-title":"Pierce and Davide Sangiorgi","author":"Benjamin","year":"1996","unstructured":"Benjamin C. Pierce and Davide Sangiorgi . 1996 . Typing and Subtyping for Mobile Processes. Mathematical Structures in Computer Science 6, 5 (1996). Benjamin C. Pierce and Davide Sangiorgi. 1996. Typing and Subtyping for Mobile Processes. Mathematical Structures in Computer Science 6, 5 (1996)."},{"key":"e_1_3_2_2_62_1","volume-title":"Rajamani and Jakob Rehof","author":"Sriram","year":"2001","unstructured":"Sriram K. Rajamani and Jakob Rehof . 2001 . A Behavioral Module System for the Pi-Calculus. In SAS. Sriram K. Rajamani and Jakob Rehof. 2001. A Behavioral Module System for the Pi-Calculus. In SAS."},{"key":"e_1_3_2_2_63_1","volume-title":"The ?-calculus: a Theory of Mobile Processes","author":"Sangiorgi Davide","unstructured":"Davide Sangiorgi and David Walker . 2001. The ?-calculus: a Theory of Mobile Processes . Cambridge University Press . Davide Sangiorgi and David Walker. 2001. The ?-calculus: a Theory of Mobile Processes. Cambridge University Press."},{"key":"e_1_3_2_2_64_1","doi-asserted-by":"crossref","unstructured":"Alceste Scalas Elias Benussi and Nobuko Yoshida. 2019. Effpi website. https:\/\/alcestes.github.io\/effpi.  Alceste Scalas Elias Benussi and Nobuko Yoshida. 2019. Effpi website. https:\/\/alcestes.github.io\/effpi.","DOI":"10.1145\/3325968"},{"key":"e_1_3_2_2_65_1","unstructured":"Alceste Scalas Ornela Dardha Raymond Hu and Nobuko Yoshida. 2017. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In ECOOP.  Alceste Scalas Ornela Dardha Raymond Hu and Nobuko Yoshida. 2017. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In ECOOP ."},{"key":"e_1_3_2_2_66_1","volume-title":"A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming (Artifact). Dagstuhl Artifacts Series 3, 1","author":"Scalas Alceste","year":"2017","unstructured":"Alceste Scalas , Ornela Dardha , Raymond Hu , and Nobuko Yoshida . 2017. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming (Artifact). Dagstuhl Artifacts Series 3, 1 ( 2017 ). Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. 2017. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming (Artifact). Dagstuhl Artifacts Series 3, 1 (2017)."},{"key":"e_1_3_2_2_67_1","unstructured":"Alceste Scalas and Nobuko Yoshida. 2016. Lightweight Session Programming in Scala. In ECOOP.  Alceste Scalas and Nobuko Yoshida. 2016. Lightweight Session Programming in Scala. In ECOOP ."},{"key":"e_1_3_2_2_68_1","volume-title":"Lightweight Session Programming in Scala (Artifact). Dagstuhl Artifacts Series 2, 1","author":"Scalas Alceste","year":"2016","unstructured":"Alceste Scalas and Nobuko Yoshida . 2016. Lightweight Session Programming in Scala (Artifact). Dagstuhl Artifacts Series 2, 1 ( 2016 ). Alceste Scalas and Nobuko Yoshida. 2016. Lightweight Session Programming in Scala (Artifact). Dagstuhl Artifacts Series 2, 1 (2016)."},{"key":"e_1_3_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290343"},{"key":"e_1_3_2_2_70_1","unstructured":"Alceste Scalas Nobuko Yoshida and Elias Benussi. 2019. Verifying message-passing programs with dependent behavioural types. https:\/\/www.doc.ic.ac.uk\/research\/technicalreports\/2019\/#1 DoC Technical report2019\/1.  Alceste Scalas Nobuko Yoshida and Elias Benussi. 2019. Verifying message-passing programs with dependent behavioural types. https:\/\/www.doc.ic.ac.uk\/research\/technicalreports\/2019\/#1 DoC Technical report2019\/1."},{"key":"e_1_3_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_3_2_2_72_1","doi-asserted-by":"crossref","unstructured":"Antal Spector-Zabusky Joachim Breitner Christine Rizkallah and Stephanie Weirich. 2018. Total Haskell is Reasonable Coq. In CPP.   Antal Spector-Zabusky Joachim Breitner Christine Rizkallah and Stephanie Weirich. 2018. Total Haskell is Reasonable Coq. In CPP .","DOI":"10.1145\/3176245.3167092"},{"key":"e_1_3_2_2_73_1","volume-title":"Modal and Temporal Properties of Processes","author":"Stirling Colin","unstructured":"Colin Stirling . 2001. Modal and Temporal Properties of Processes . Springer-Verlag New York, Inc. , New York, NY, USA . Colin Stirling. 2001. Modal and Temporal Properties of Processes. Springer-Verlag New York, Inc., New York, NY, USA."},{"key":"e_1_3_2_2_74_1","doi-asserted-by":"crossref","unstructured":"Marcelo Taube Giuliano Losa Kenneth L. McMillan Oded Padon Mooly Sagiv Sharon Shoham James R. Wilcox and Doug Woos. 2018. Modularity for decidability of deductive verification with applications to distributed systems. In PLDI.   Marcelo Taube Giuliano Losa Kenneth L. McMillan Oded Padon Mooly Sagiv Sharon Shoham James R. Wilcox and Doug Woos. 2018. Modularity for decidability of deductive verification with applications to distributed systems. In PLDI .","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_3_2_2_75_1","doi-asserted-by":"crossref","unstructured":"Bernardo. Toninho Luis. Caires and Frank Pfenning. 2011. Dependent session types via intuitionistic linear type theory. In PPDP.   Bernardo. Toninho Luis. Caires and Frank Pfenning. 2011. Dependent session types via intuitionistic linear type theory. In PPDP .","DOI":"10.1145\/2003476.2003499"},{"key":"e_1_3_2_2_76_1","volume-title":"C","author":"Toninho Bernardo","year":"2017","unstructured":"Bernardo Toninho and Nobuko Yoshida . 2017. Certifying data in multiparty session types. Journal of Logical and Algebraic Methods in Programming 90 , C ( 2017 ). Bernardo Toninho and Nobuko Yoshida. 2017. Certifying data in multiparty session types. Journal of Logical and Algebraic Methods in Programming 90, C (2017)."},{"key":"e_1_3_2_2_77_1","doi-asserted-by":"crossref","unstructured":"Bernardo Toninho and Nobuko Yoshida. 2018. Depending on Session-Typed Processes. In FoSSaCS.  Bernardo Toninho and Nobuko Yoshida. 2018. Depending on Session-Typed Processes. In FoSSaCS .","DOI":"10.1007\/978-3-319-89366-2_7"},{"key":"e_1_3_2_2_78_1","doi-asserted-by":"crossref","unstructured":"Nobuko Yoshida. 2004. Channel dependent types for higher-order mobile processes. In POPL.   Nobuko Yoshida. 2004. Channel dependent types for higher-order mobile processes. In POPL .","DOI":"10.1145\/964001.964014"},{"key":"e_1_3_2_2_79_1","volume-title":"Assigning Types to Processes. Information and Computation 174, 2","author":"Yoshida Nobuko","year":"2002","unstructured":"Nobuko Yoshida and Matthew Hennessy . 2002. Assigning Types to Processes. Information and Computation 174, 2 ( 2002 ). Nobuko Yoshida and Matthew Hennessy. 2002. Assigning Types to Processes. Information and Computation 174, 2 (2002)."}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3322484","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3322484","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:29Z","timestamp":1750204409000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3322484"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":79,"alternative-id":["10.1145\/3314221.3322484","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3322484","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}