{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T18:14:14Z","timestamp":1744222454624},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"National Science Foundation","award":["1801369"]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"Traditional session types prescribe bidirectional communication protocols for\nconcurrent computations, where well-typed programs are guaranteed to adhere to\nthe protocols. However, simple session types cannot capture properties beyond\nthe basic type of the exchanged messages. In response, recent work has extended\nsession types with refinements from linear arithmetic, capturing intrinsic\nattributes of processes and data. These refinements then play a central role in\ndescribing sequential and parallel complexity bounds on session-typed programs.\nThe Rast language provides an open-source implementation of session-typed\nconcurrent programs extended with arithmetic refinements as well as ergometric\nand temporal types to capture work and span of program execution. To further\nsupport generic programming, Rast also enhances arithmetically refined session\ntypes with recently developed nested parametric polymorphism. Type checking\nrelies on Cooper's algorithm for quantifier elimination in Presburger\narithmetic with a few significant optimizations, and a heuristic extension to\nnonlinear constraints. Rast furthermore includes a reconstruction engine so\nthat most program constructs pertaining the layers of refinements and resources\nare inserted automatically. We provide a variety of examples to demonstrate the\nexpressivity of the language.<\/jats:p>","DOI":"10.46298\/lmcs-18(1:9)2022","type":"journal-article","created":{"date-parts":[[2022,1,13]],"date-time":"2022-01-13T17:31:51Z","timestamp":1642095111000},"source":"Crossref","is-referenced-by-count":7,"title":["Rast: A Language for Resource-Aware Session Types"],"prefix":"10.46298","volume":"Volume 18, Issue 1","author":[{"given":"Ankush","family":"Das","sequence":"first","affiliation":[]},{"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2022,1,12]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/8954\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/8954\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:19:14Z","timestamp":1687292354000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/7024"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-18(1:9)2022","relation":{"has-preprint":[{"id-type":"arxiv","id":"2012.13129v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2012.13129v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2012.13129","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2012.13129","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]}}}