{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:59Z","timestamp":1779836759373,"version":"3.53.1"},"reference-count":36,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2022,2,28]],"date-time":"2022-02-28T00:00:00Z","timestamp":1646006400000},"content-version":"unspecified","delay-in-days":58,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Common approaches to concurrent programming begin with languages whose semantics are naturally sequential and add new constructs that provide limited access to concurrency, as exemplified by\n                    <jats:italic>futures<\/jats:italic>\n                    . This approach has been quite successful, but often does not provide a satisfactory theoretical backing for the concurrency constructs, and it can be difficult to give a good semantics that allows a programmer to use more than one of these constructs at a time. We take a different approach, starting with a concurrent language based on a Curry\u2013Howard interpretation of adjoint logic, to which we add three atomic primitives that allow us to encode sequential composition and various forms of synchronization. The resulting language is highly expressive, allowing us to encode futures, fork\/join parallelism, and monadic concurrency in the same framework. Notably, since our language is based on adjoint logic, we are able to give a formal account of\n                    <jats:italic>linear futures<\/jats:italic>\n                    , which have been used in complexity analysis by Blelloch and Reid-Miller. The uniformity of this approach means that we can similarly work with many of the other concurrency primitives in a linear fashion, and that we can mix several of these forms of concurrency in the same program to serve different purposes.\n                  <\/jats:p>","DOI":"10.1017\/s0956796822000016","type":"journal-article","created":{"date-parts":[[2022,2,28]],"date-time":"2022-02-28T09:32:50Z","timestamp":1646040770000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":5,"title":["Back to futures"],"prefix":"10.1017","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6032-087X","authenticated-orcid":false,"given":"KLAAS","family":"PRUIKSMA","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"FRANK","family":"PFENNING","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2022,2,28]]},"reference":[{"key":"S0956796822000016_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022251"},{"key":"S0956796822000016_ref7","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1936-1501858-0"},{"key":"S0956796822000016_ref6","volume-title":"A Concurrent Logical Framework II: Examples and Applications","author":"Cervesato","year":"2002"},{"key":"S0956796822000016_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00173-5"},{"key":"S0956796822000016_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837652"},{"key":"S0956796822000016_ref26","unstructured":"Licata, D. R. , Shulman, M. & Riley, M. (2017) A fibrational framework for substructural and modal logics. In Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD\u201917), Miller, D. (ed). LIPIcs, pp. 25:1\u201325:22."},{"key":"S0956796822000016_ref10","unstructured":"Das, A. & Pfenning, F. (2020) Rast: Resource-aware session types with arithmetic refinements. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Ariola, Z. (ed). LIPIcs 167, pp. 33:1\u201333:17. System description."},{"key":"S0956796822000016_ref18","doi-asserted-by":"publisher","DOI":"10.2172\/1562827"},{"key":"S0956796822000016_ref32","unstructured":"Reed, J. (2009) A Judgmental Deconstruction of Modal Logic. Unpublished manuscript."},{"key":"S0956796822000016_ref30","unstructured":"Pruiksma, K. & Pfenning, F. (2020) Back to futures. CoRR abs\/2002.04607(Feb.)."},{"key":"S0956796822000016_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/1463822.1463838"},{"key":"S0956796822000016_ref36","first-page":"45","volume-title":"Conference on Lisp and Functional Programming (LFP 1984)","author":"Wadler","year":"1984"},{"key":"S0956796822000016_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"S0956796822000016_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s002240000117"},{"key":"S0956796822000016_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"S0956796822000016_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"S0956796822000016_ref11","unstructured":"DeYoung, H. , Pfenning, F. & Pruiksma, K. (2020) Semi-axiomatic sequent calculus. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Ariola, Z. (ed). LIPIcs 167, pp. 29:1\u201329:22."},{"key":"S0956796822000016_ref29","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.291.6"},{"key":"S0956796822000016_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2986012.2986014"},{"key":"S0956796822000016_ref12","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2627"},{"key":"S0956796822000016_ref31","unstructured":"Pruiksma, K. , Chargin, W. , Pfenning, F. & Reed, J. (2018) Adjoint Logic. Unpublished manuscript."},{"key":"S0956796822000016_ref27","first-page":"235","volume-title":"7th Annual Symposium on Logic in Computer Science (LICS 1992)","author":"Lincoln","year":"1992"},{"key":"S0956796822000016_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"S0956796822000016_ref33","unstructured":"Simmons, R. J. (2012) Substructural Logical Specifications. PhD thesis, Carnegie Mellon University. Available as Technical Report CMU-CS-12-142."},{"key":"S0956796822000016_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/4472.4478"},{"key":"S0956796822000016_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.11.006"},{"key":"S0956796822000016_ref20","volume-title":"Grundlagen der Mathematik","author":"Hilbert","year":"1934"},{"key":"S0956796822000016_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014972"},{"key":"S0956796822000016_ref24","unstructured":"Larus, J. R. (1989) Restructuring Symbolic Programs for Concurrent Execution on Multiprocessors. PhD thesis, University of California, Berkeley."},{"key":"S0956796822000016_ref34","unstructured":"Toninho, B. (2015) A Logical Foundation for Session-based Concurrent Computation. PhD thesis, Carnegie Mellon University and Universidade Nova de Lisboa. Available as Technical Report CMU-CS-15-109."},{"key":"S0956796822000016_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-27683-0_16"},{"key":"S0956796822000016_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"key":"S0956796822000016_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192391"},{"key":"S0956796822000016_ref16","doi-asserted-by":"crossref","unstructured":"Gentzen, G. (1935) Untersuchungen \u00dcber das logische Schlie\u00dfen. Math. Z. 39, 176\u2013210, 405\u2013431. English translation in M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pp. 68\u2013131, North-Holland, 1969.","DOI":"10.1007\/BF01201363"},{"key":"S0956796822000016_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_20"},{"key":"S0956796822000016_ref23","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.322.7"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796822000016","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:58Z","timestamp":1779835018000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796822000016\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"references-count":36,"alternative-id":["S0956796822000016"],"URL":"https:\/\/doi.org\/10.1017\/s0956796822000016","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e6"}}