{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:47Z","timestamp":1780994747160,"version":"3.54.1"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2022,9,15]],"date-time":"2022-09-15T00:00:00Z","timestamp":1663200000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Imperative session types provide an imperative interface to session-typed\ncommunication. In such an interface, channel references are first-class objects\nwith operations that change the typestate of the channel. Compared to\nfunctional session type APIs, the program structure is simpler at the surface,\nbut typestate is required to model the current state of communication\nthroughout. Following an early work that explored the imperative approach, a\nsignificant body of work on session types has neglected the imperative approach\nand opts for a functional approach that uses linear types to manage channel\nreferences soundly. We demonstrate that the functional approach subsumes the\nearly work on imperative session types by exhibiting a typing and semantics\npreserving translation into a system of linear functional session types. We\nfurther show that the untyped backwards translation from the functional to the\nimperative calculus is semantics preserving. We restrict the type system of the\nfunctional calculus such that the backwards translation becomes type\npreserving. Thus, we precisely capture the difference in expressiveness of the\ntwo calculi and conclude that the lack of expressiveness in the imperative\ncalculus is largely due to restrictions imposed by its type system.<\/jats:p>","DOI":"10.46298\/lmcs-18(3:33)2022","type":"journal-article","created":{"date-parts":[[2022,9,19]],"date-time":"2022-09-19T07:36:05Z","timestamp":1663572965000},"source":"Crossref","is-referenced-by-count":3,"title":["Relating Functional and Imperative Session Types"],"prefix":"10.46298","volume":"Volume 18, Issue 3","author":[{"given":"Hannes","family":"Saffrich","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"Thiemann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2022,9,15]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/10045\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/10045\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:20:38Z","timestamp":1687292438000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/8815"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,15]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-18(3:33)2022","relation":{"has-preprint":[{"id-type":"arxiv","id":"2010.08261v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2010.08261v2","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2010.08261","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2010.08261","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,9,15]]},"article-number":"8815"}}