{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:34:24Z","timestamp":1753889664143,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,10,5]],"date-time":"2012-10-05T00:00:00Z","timestamp":1349395200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The enriched effect calculus (EEC) is an extension of Moggi's computational\nmetalanguage with a selection of primitives from linear logic. This paper\nexplores the enriched effect calculus as a target language for\ncontinuation-passing-style (CPS) translations in which the typing of the\ntranslations enforces the linear usage of continuations. We first observe that\nestablished call-by-value and call-by name linear-use CPS translations of\nsimply-typed lambda-calculus into intuitionistic linear logic (ILL) land in the\nfragment of ILL given by EEC. These two translations are uniformly generalised\nby a single generic translation of the enriched effect calculus into itself. As\nour main theorem, we prove that the generic self-translation of EEC is\ninvolutive up to isomorphism. As corollaries, we obtain full completeness\nresults, both for the generic translation, and for the original call-by-value\nand call-by-name translations.<\/jats:p>","DOI":"10.2168\/lmcs-8(4:2)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T13:21:33Z","timestamp":1385731293000},"source":"Crossref","is-referenced-by-count":0,"title":["Linear-use CPS translations in the Enriched Effect Calculus"],"prefix":"10.46298","volume":"Volume 8, Issue 4","author":[{"given":"Jeff","family":"Egger","sequence":"first","affiliation":[]},{"given":"Rasmus Ejlers","family":"M\u00f8gelberg","sequence":"additional","affiliation":[]},{"given":"Alex","family":"Simpson","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,10,5]]},"reference":[{"key":"580:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/923\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/923\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:59:07Z","timestamp":1681243147000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/923"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,5]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(4:2)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1209.4268","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1209.4268","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,10,5]]},"article-number":"923"}}