{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:21:59Z","timestamp":1750220519861,"version":"3.41.0"},"reference-count":77,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2021,6,10]],"date-time":"2021-06-10T00:00:00Z","timestamp":1623283200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100021680","name":"NOVA LINCS","doi-asserted-by":"crossref","award":["UID\/CEC\/04516\/2019, UIDB\/04516\/2020), EPSRC EP\/N028201\/1, EP\/K034413\/1, EP\/K011715\/1, EP\/L00058X\/1, EP\/N027833\/1, EP\/T006544\/1, EP\/T014709\/1, EP\/V000462\/1 and EPSRC\/NCSC\/GCHQ VeTSS."],"award-info":[{"award-number":["UID\/CEC\/04516\/2019, UIDB\/04516\/2020), EPSRC EP\/N028201\/1, EP\/K034413\/1, EP\/K011715\/1, EP\/L00058X\/1, EP\/N027833\/1, EP\/T006544\/1, EP\/T014709\/1, EP\/V000462\/1 and EPSRC\/NCSC\/GCHQ VeTSS."]}],"id":[{"id":"10.13039\/501100021680","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2021,6,30]]},"abstract":"<jats:p>\n            This work exploits the logical foundation of session types to determine what kind of type discipline for the \u039b-calculus can exactly capture, and is captured by, \u039b-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first\n            <jats:italic>mutually inverse<\/jats:italic>\n            and\n            <jats:italic>fully abstract<\/jats:italic>\n            processes-as-functions and functions-as-processes encodings between a polymorphic session \u03c0-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the \u039b-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for\n            <jats:italic>value<\/jats:italic>\n            and\n            <jats:italic>process<\/jats:italic>\n            passing, entailing strong normalisation.\n          <\/jats:p>","DOI":"10.1145\/3457884","type":"journal-article","created":{"date-parts":[[2021,6,10]],"date-time":"2021-06-10T16:18:09Z","timestamp":1623341889000},"page":"1-55","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["On Polymorphic Sessions and Functions"],"prefix":"10.1145","volume":"43","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0746-7514","authenticated-orcid":false,"given":"Bernardo","family":"Toninho","sequence":"first","affiliation":[{"name":"NOVA-LINCS and NOVA School of Science and Technology, Portugal"}]},{"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[{"name":"Imperial College London, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2021,6,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000031"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90151-7"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110281"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2018.30"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022251"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of TLCA\u201901","volume":"2044","author":"Berger Martin","year":"2001","unstructured":"Martin Berger, Kohei Honda, and Nobuko Yoshida. 2001. Sequentiality and the -calculus. In Proceedings of TLCA\u201901.Lecture Notes in Computer Science (LNCS), vol. 2044. Springer, 29\u201345."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0175-1"},{"volume-title":"The Algebra of Programming","author":"Bird Richard","key":"e_1_2_1_9_1","unstructured":"Richard Bird and Oege De Moor. 1997. The Algebra of Programming. Prentice-Hall."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(5:2)2006"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_19"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000218"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2016.33"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.412"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2370776.2370794"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Romain Demangeon Daniel Hirschkoff and Davide Sangiorgi. 2009. Mobile processes and termination. In Semantics and Algebraic Specification. 250\u2013273.","DOI":"10.1007\/978-3-642-04164-8_13"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.07.007"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.14"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290341"},{"key":"e_1_2_1_21_1","volume-title":"Behavioural Types: From Theory to Tools","author":"Gay Simon","year":"2017","unstructured":"Simon Gay and Antonio Ravara (Eds.). 2017. Behavioural Types: From Theory to Tools. River Publishers."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_24_1","unstructured":"Jean-Yves Girard Yves Lafont and Paul Taylor. 1989. Proofs and Types. Cambridge University Press."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.05.002"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000279"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000372"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_4"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.9"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-59746-1_6"},{"key":"e_1_2_1_34_1","volume-title":"Session-Ocaml: A session-based library with polarities and lenses. scico","author":"Imai Keigo","year":"2019","unstructured":"Keigo Imai, Nobuko Yoshida, and Shoji Yuen. 2019. Session-Ocaml: A session-based library with polarities and lenses. scico (2019), 1\u201350."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_18"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_23"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951921"},{"volume-title":"Behavioural Types: From Theory to Tools","author":"Lindley Sam","key":"e_1_2_1_38_1","unstructured":"Sam Lindley and J. Garrett Morris. 2017. Lightweight functional session types. In Behavioural Types: From Theory to Tools. River Publishers."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00358-2"},{"key":"e_1_2_1_40_1","volume-title":"Symposium on Logic in Computer Science (LICS \u201987)","author":"Mendler N. P.","year":"1987","unstructured":"N. P. Mendler. 1987. Recursive types and type constraints in second-order lambda calculus. In Symposium on Logic in Computer Science (LICS \u201987) (Ithaca, New York, , June 22-25, 1987). 30\u201336."},{"key":"e_1_2_1_41_1","unstructured":"Robin Miler. 2001. Speech on receiving an Honorary Degree from the University of Bologna. www.cs.unibo.it\/icalp\/Lauree_milner.html."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001407"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2868"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_13"},{"volume-title":"Behavioural Types: From Theory to Tools","author":"Orchard Dominic","key":"e_1_2_1_46_1","unstructured":"Dominic Orchard and Nobuko Yoshida. 2017. Session types with linearity in Haskell. In Behavioural Types: From Theory to Tools. River Publishers."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837634"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_30"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.011"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_27"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.08.001"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.300.2"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_1"},{"volume-title":"Advanced Topics in Types and Programming Languages","author":"Pierce Benjamin C.","key":"e_1_2_1_54_1","unstructured":"Benjamin C. Pierce. 2004. Advanced Topics in Types and Programming Languages. The MIT Press."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950007002X"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/337244.337261"},{"key":"e_1_2_1_57_1","volume-title":"Turner","author":"Pierce Benhamin C.","year":"1990","unstructured":"Benhamin C. Pierce and David N. Turner. 1990. Pict Programming Language homepage. https:\/\/www.cis.upenn.edu\/ bcpierce\/papers\/pict\/Html\/Pict.html."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037118"},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the IFIP 9th World Computer Congress","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds. 1983. Types, abstraction and parametric polymorphism. In Information Processing 83, Proceedings of the IFIP 9th World Computer Congress (Paris, France, September 19-23, 1983).513\u2013523."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1037"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56610-4_62"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58027-1_7"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00075-8"},{"key":"e_1_2_1_64_1","doi-asserted-by":"crossref","unstructured":"Davide Sangiorgi. 2000. Lazy functions and mobile processes. In Proof Language and Interaction Essays in Honour of Robin Milner. 691\u2013720.","DOI":"10.7551\/mitpress\/5641.003.0033"},{"volume-title":"The Pi-Calculus - A Theory of Mobile Processes","author":"Sangiorgi Davide","key":"e_1_2_1_65_1","unstructured":"Davide Sangiorgi and David Walker. 2001. The Pi-Calculus - A Theory of Mobile Processes. Cambridge University Press."},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_7"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.24"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2016.21"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.238.7"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28729-9_23"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_20"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45917-1_11"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_29"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","unstructured":"Bernardo Toninho and Nobuko Yoshida. 2019. Polymorphic session processes as morphisms. In The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy - Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday. 101\u2013117. DOI:https:\/\/doi.org\/10.1007\/978-3-030-31175-9_7","DOI":"10.1007\/978-3-030-31175-9_7"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681400001X"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.238.8"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.08.004"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17164-2_24"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3457884","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3457884","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:38Z","timestamp":1750195478000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3457884"}},"subtitle":["A Tale of Two (Fully Abstract) Encodings"],"short-title":[],"issued":{"date-parts":[[2021,6,10]]},"references-count":77,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,6,30]]}},"alternative-id":["10.1145\/3457884"],"URL":"https:\/\/doi.org\/10.1145\/3457884","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2021,6,10]]},"assertion":[{"value":"2019-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-06-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}