{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:49:32Z","timestamp":1775868572546,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,9,6]],"date-time":"2021-09-06T00:00:00Z","timestamp":1630886400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e Tecnologia, IP","award":["UIDB\/04516\/2020"],"award-info":[{"award-number":["UIDB\/04516\/2020"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,9,6]]},"DOI":"10.1145\/3479394.3479398","type":"proceedings-article","created":{"date-parts":[[2021,10,7]],"date-time":"2021-10-07T22:23:02Z","timestamp":1633645382000},"page":"1-3","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["A Decade of Dependent Session Types"],"prefix":"10.1145","author":[{"given":"Bernardo","family":"Toninho","sequence":"first","affiliation":[{"name":"NOVA School of Science and Technology and NOVA-LINCS, Portugal"}]},{"given":"Lu\u00eds","family":"Caires","sequence":"additional","affiliation":[{"name":"NOVA School of Science and Technology and NOVA-LINCS, Portugal"}]},{"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,10,7]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, Sam Lindley, Conor McBride, Philip\u00a0W","author":"Atkey Robert","unstructured":"Robert Atkey , Sam Lindley , and J.\u00a0 Garrett Morris . 2016. Conflation Confers Concurrency . In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, Sam Lindley, Conor McBride, Philip\u00a0W . Trinder, and Donald Sannella (Eds.). Springer , 32\u201355. https:\/\/doi.org\/10.1007\/978-3-319-30936-1_2 10.1007\/978-3-319-30936-1_2 Robert Atkey, Sam Lindley, and J.\u00a0Garrett Morris. 2016. Conflation Confers Concurrency. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, Sam Lindley, Conor McBride, Philip\u00a0W. Trinder, and Donald Sannella (Eds.). Springer, 32\u201355. https:\/\/doi.org\/10.1007\/978-3-319-30936-1_2"},{"key":"e_1_3_2_1_2_1","volume-title":"Proc. ACM Program. Lang. 1, ICFP","author":"Balzer Stephanie","year":"2017","unstructured":"Stephanie Balzer and Frank Pfenning . 2017 . Manifest sharing with session types . Proc. ACM Program. Lang. 1, ICFP (2017), 37:1\u201337:29. https:\/\/doi.org\/10.1145\/3110281 10.1145\/3110281 Stephanie Balzer and Frank Pfenning. 2017. Manifest sharing with session types. Proc. ACM Program. Lang. 1, ICFP (2017), 37:1\u201337:29. https:\/\/doi.org\/10.1145\/3110281"},{"key":"e_1_3_2_1_3_1","volume-title":"Manifest Deadlock-Freedom for Shared Session Types. In 28th European Symposium on Programming, ESOP","author":"Balzer Stephanie","year":"2019","unstructured":"Stephanie Balzer , Bernardo Toninho , and Frank Pfenning . 2019 . Manifest Deadlock-Freedom for Shared Session Types. In 28th European Symposium on Programming, ESOP 2019, Lu\u00eds Caires (Ed.). Springer, 611\u2013639. https:\/\/doi.org\/10.1007\/978-3-030-17184-1_22 10.1007\/978-3-030-17184-1_22 Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. 2019. Manifest Deadlock-Freedom for Shared Session Types. In 28th European Symposium on Programming, ESOP 2019, Lu\u00eds Caires (Ed.). Springer, 611\u2013639. https:\/\/doi.org\/10.1007\/978-3-030-17184-1_22"},{"key":"e_1_3_2_1_4_1","volume-title":"CONCUR 2010 - Concurrency Theory, 21th International Conference, Paul Gastin and Fran\u00e7ois Laroussinie (Eds.). Springer, 162\u2013176","author":"Bocchi Laura","year":"2010","unstructured":"Laura Bocchi , Kohei Honda , Emilio Tuosto , and Nobuko Yoshida . 2010 . A Theory of Design-by-Contract for Distributed Multiparty Interactions . In CONCUR 2010 - Concurrency Theory, 21th International Conference, Paul Gastin and Fran\u00e7ois Laroussinie (Eds.). Springer, 162\u2013176 . https:\/\/doi.org\/10.1007\/978-3-642-15375-4_12 10.1007\/978-3-642-15375-4_12 Laura Bocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida. 2010. A Theory of Design-by-Contract for Distributed Multiparty Interactions. In CONCUR 2010 - Concurrency Theory, 21th International Conference, Paul Gastin and Fran\u00e7ois Laroussinie (Eds.). Springer, 162\u2013176. https:\/\/doi.org\/10.1007\/978-3-642-15375-4_12"},{"key":"e_1_3_2_1_5_1","volume-title":"CONCUR 2010 - Concurrency Theory, 21th International Conference, Paul Gastin and Fran\u00e7ois Laroussinie (Eds.). Springer, 222\u2013236","author":"Caires Lu\u00eds","year":"2010","unstructured":"Lu\u00eds Caires and Frank Pfenning . 2010 . Session Types as Intuitionistic Linear Propositions . In CONCUR 2010 - Concurrency Theory, 21th International Conference, Paul Gastin and Fran\u00e7ois Laroussinie (Eds.). Springer, 222\u2013236 . https:\/\/doi.org\/10.1007\/978-3-642-15375-4_16 10.1007\/978-3-642-15375-4_16 Lu\u00eds Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In CONCUR 2010 - Concurrency Theory, 21th International Conference, Paul Gastin and Fran\u00e7ois Laroussinie (Eds.). Springer, 222\u2013236. https:\/\/doi.org\/10.1007\/978-3-642-15375-4_16"},{"key":"e_1_3_2_1_6_1","volume-title":"TLDI 2012: 7th ACM SIGPLAN Workshop on Types in Languages Design and Implementation, Benjamin\u00a0C. Pierce (Ed.). ACM, 1\u201312","author":"Caires Lu\u00eds","year":"2012","unstructured":"Lu\u00eds Caires , Frank Pfenning , and Bernardo Toninho . 2012 . Towards concurrent type theory . In TLDI 2012: 7th ACM SIGPLAN Workshop on Types in Languages Design and Implementation, Benjamin\u00a0C. Pierce (Ed.). ACM, 1\u201312 . https:\/\/doi.org\/10.1145\/2103786.2103788 10.1145\/2103786.2103788 Lu\u00eds Caires, Frank Pfenning, and Bernardo Toninho. 2012. Towards concurrent type theory. In TLDI 2012: 7th ACM SIGPLAN Workshop on Types in Languages Design and Implementation, Benjamin\u00a0C. Pierce (Ed.). ACM, 1\u201312. https:\/\/doi.org\/10.1145\/2103786.2103788"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000218"},{"key":"e_1_3_2_1_8_1","volume-title":"FOSSACS","author":"Dardha Ornela","year":"2018","unstructured":"Ornela Dardha and Simon\u00a0 J. Gay . 2018 . A New Linear Logic for Deadlock-Free Session-Typed Processes. In Foundations of Software Science and Computation Structures - 21st International Conference , FOSSACS 2018, Christel Baier and Ugo\u00a0Dal Lago (Eds.). Springer, 91\u2013109. https:\/\/doi.org\/10.1007\/978-3-319-89366-2_5 10.1007\/978-3-319-89366-2_5 Ornela Dardha and Simon\u00a0J. Gay. 2018. A New Linear Logic for Deadlock-Free Session-Typed Processes. In Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Christel Baier and Ugo\u00a0Dal Lago (Eds.). Springer, 91\u2013109. https:\/\/doi.org\/10.1007\/978-3-319-89366-2_5"},{"key":"e_1_3_2_1_9_1","volume-title":"Nested Session Types. In 30th European Symposium on Programming, ESOP 2021","author":"Das Ankush","year":"2021","unstructured":"Ankush Das , Henry DeYoung , Andreia Mordido , and Frank Pfenning . 2021 . Nested Session Types. In 30th European Symposium on Programming, ESOP 2021 , Nobuko Yoshida (Ed.). Springer, 178\u2013206. https:\/\/doi.org\/10.1007\/978-3-030-7 2019-3_7 10.1007\/978-3-030-72019-3_7 Ankush Das, Henry DeYoung, Andreia Mordido, and Frank Pfenning. 2021. Nested Session Types. In 30th European Symposium on Programming, ESOP 2021, Nobuko Yoshida (Ed.). Springer, 178\u2013206. https:\/\/doi.org\/10.1007\/978-3-030-72019-3_7"},{"key":"e_1_3_2_1_10_1","volume-title":"Proc. ACM Program. Lang. 2, ICFP","author":"Das Ankush","year":"2018","unstructured":"Ankush Das , Jan Hoffmann , and Frank Pfenning . 2018 . Parallel complexity analysis with temporal session types . Proc. ACM Program. Lang. 2, ICFP (2018), 91:1\u201391:30. https:\/\/doi.org\/10.1145\/3236786 10.1145\/3236786 Ankush Das, Jan Hoffmann, and Frank Pfenning. 2018. Parallel complexity analysis with temporal session types. Proc. ACM Program. Lang. 2, ICFP (2018), 91:1\u201391:30. https:\/\/doi.org\/10.1145\/3236786"},{"key":"e_1_3_2_1_11_1","volume-title":"Work Analysis with Resource-Aware Session Types. In 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018","author":"Das Ankush","year":"2018","unstructured":"Ankush Das , Jan Hoffmann , and Frank Pfenning . 2018 . Work Analysis with Resource-Aware Session Types. In 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018 , Anuj Dawar and Erich Gr\u00e4del (Eds.). ACM, 305\u2013314. https:\/\/doi.org\/10.1145\/3 209108.3209146 10.1145\/3209108.3209146 Ankush Das, Jan Hoffmann, and Frank Pfenning. 2018. Work Analysis with Resource-Aware Session Types. In 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Anuj Dawar and Erich Gr\u00e4del (Eds.). ACM, 305\u2013314. https:\/\/doi.org\/10.1145\/3209108.3209146"},{"key":"e_1_3_2_1_12_1","first-page":"1","article-title":"Session Types with Arithmetic Refinements. In CONCUR 2020 - Concurrency Theory, 31th International Conference, Igor Konnovand Laura Kov\u00e1cs (Eds.)","volume":"13","author":"Das Ankush","year":"2020","unstructured":"Ankush Das and Frank Pfenning . 2020 . Session Types with Arithmetic Refinements. In CONCUR 2020 - Concurrency Theory, 31th International Conference, Igor Konnovand Laura Kov\u00e1cs (Eds.) . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik , 13 : 1 \u2013 13 :18. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.13 10.4230\/LIPIcs.CONCUR.2020.13 Ankush Das and Frank Pfenning. 2020. Session Types with Arithmetic Refinements. In CONCUR 2020 - Concurrency Theory, 31th International Conference, Igor Konnovand Laura Kov\u00e1cs (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 13:1\u201313:18. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.13","journal-title":"Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3414080.3414087"},{"key":"e_1_3_2_1_14_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":"Vasconcelos T.","year":"1998","unstructured":"Kohei. Honda, Vasco\u00a0 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\u00a0T. 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_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_3_2_1_16_1","volume-title":"21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016","author":"Lindley Sam","year":"2016","unstructured":"Sam Lindley and J.\u00a0 Garrett Morris . 2016 . Talking bananas: structural recursion for session types . In 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016 , Jacques Garrigue, Gabriele Keller, and Eijiro Sumii(Eds.). ACM, 434\u2013447. https:\/\/doi.org\/10.1145\/295 1913.2951921 10.1145\/2951913.2951921 Sam Lindley and J.\u00a0Garrett Morris. 2016. Talking bananas: structural recursion for session types. In 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Jacques Garrigue, Gabriele Keller, and Eijiro Sumii(Eds.). ACM, 434\u2013447. https:\/\/doi.org\/10.1145\/2951913.2951921"},{"key":"e_1_3_2_1_17_1","volume-title":"27th International Conf. on Compiler Construction, CC","author":"Neykova Rumyana","year":"2018","unstructured":"Rumyana Neykova , Raymond Hu , Nobuko Yoshida , and Fahd Abdeljallal . 2018 . A session type provider: compile-time API generation of distributed protocols with refinements in F# . In 27th International Conf. on Compiler Construction, CC 2018, Christophe Dubach and Jingling Xue (Eds.). ACM, 128\u2013138. https:\/\/doi.org\/10.1145\/3178372.3179495 10.1145\/3178372.3179495 Rumyana Neykova, Raymond Hu, Nobuko Yoshida, and Fahd Abdeljallal. 2018. A session type provider: compile-time API generation of distributed protocols with refinements in F#. In 27th International Conf. on Compiler Construction, CC 2018, Christophe Dubach and Jingling Xue (Eds.). ACM, 128\u2013138. https:\/\/doi.org\/10.1145\/3178372.3179495"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_4"},{"key":"e_1_3_2_1_19_1","volume-title":"Proc. ACM Program. Lang. 5, ICFP.","author":"Rocha Pedro","year":"2021","unstructured":"Pedro Rocha and Lu\u00eds Caires . 2021 . Propositions-as-Types and Shared State . Proc. ACM Program. Lang. 5, ICFP. to appear. Pedro Rocha and Lu\u00eds Caires. 2021. Propositions-as-Types and Shared State. Proc. ACM Program. Lang. 5, ICFP. to appear."},{"key":"e_1_3_2_1_20_1","unstructured":"Siva Somayyajula and Frank Pfenning. 2021. Circular Proofs as Processes: Type-Based Termination via Arithmetic Refinements. (2021). https:\/\/arxiv.org\/abs\/2105.06024  Siva Somayyajula and Frank Pfenning. 2021. Circular Proofs as Processes: Type-Based Termination via Arithmetic Refinements. (2021). https:\/\/arxiv.org\/abs\/2105.06024"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371135"},{"key":"e_1_3_2_1_22_1","volume-title":"13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Peter Schneider-Kamp and Michael Hanus (Eds.). ACM, 161\u2013172","author":"Toninho Bernardo","year":"2011","unstructured":"Bernardo Toninho , Lu\u00eds Caires , and Frank Pfenning . 2011 . Dependent session types via intuitionistic linear type theory . In 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Peter Schneider-Kamp and Michael Hanus (Eds.). ACM, 161\u2013172 . https:\/\/doi.org\/10.1145\/2003476.2003499 10.1145\/2003476.2003499 Bernardo Toninho, Lu\u00eds Caires, and Frank Pfenning. 2011. Dependent session types via intuitionistic linear type theory. In 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Peter Schneider-Kamp and Michael Hanus (Eds.). ACM, 161\u2013172. https:\/\/doi.org\/10.1145\/2003476.2003499"},{"key":"e_1_3_2_1_23_1","volume-title":"TGC","author":"Toninho Bernardo","year":"2014","unstructured":"Bernardo Toninho , Lu\u00eds Caires , and Frank Pfenning . 2014 . Corecursion and Non-divergence in Session-Typed Processes. In Trustworthy Global Computing - 9th International Symposium , TGC 2014, Revised Selected Papers, Matteo Maffei and Emilio Tuosto (Eds.). Springer, 159\u2013175. https:\/\/doi.org\/10.1007\/978-3-662-45917-1_11 10.1007\/978-3-662-45917-1_11 Bernardo Toninho, Lu\u00eds Caires, and Frank Pfenning. 2014. Corecursion and Non-divergence in Session-Typed Processes. In Trustworthy Global Computing - 9th International Symposium, TGC 2014, Revised Selected Papers, Matteo Maffei and Emilio Tuosto (Eds.). Springer, 159\u2013175. https:\/\/doi.org\/10.1007\/978-3-662-45917-1_11"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.11.005"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364568"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428216"}],"event":{"name":"PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming","location":"Tallinn Estonia","acronym":"PPDP 2021"},"container-title":["23rd International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3479394.3479398","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3479394.3479398","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:52Z","timestamp":1750191532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3479394.3479398"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,6]]},"references-count":26,"alternative-id":["10.1145\/3479394.3479398","10.1145\/3479394"],"URL":"https:\/\/doi.org\/10.1145\/3479394.3479398","relation":{},"subject":[],"published":{"date-parts":[[2021,9,6]]},"assertion":[{"value":"2021-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}