A Continuation-Based Solution of the Linearity Challenge

A Continuation-Based Solution of the Linearity Challenge | Research Square window.SnipcartSettings = { analytics: { enabled: false } }; (function() { var accessVector = localStorage.getItem('access_vector') || ''; window.dataLayer = window.dataLayer || []; if (accessVector) { window.dataLayer.push({ user: { profile: { profileInfo: { snid: accessVector } } } }); } })(); (function(w,d,s,l,i){w[l]=w[l]||[];w[l].push({'gtm.start':new Date().getTime(),event:'gtm.js'});var f=d.getElementsByTagName(s)[0],j=d.createElement(s),dl=l!='dataLayer'?'&l='+l:'';j.async=true;j.src='https://www.googletagmanager.com/gtm.js?id='+i+dl;f.parentNode.insertBefore(j,f);})(window,document,'script','dataLayer','GTM-K279D39R'); Browse Preprints In Review Journals COVID-19 Preprints AJE Video Bytes Research Tools Research Promotion AJE Professional Editing AJE Rubriq About Preprint Platform In Review Editorial Policies Our Team Advisory Board Help Center Sign In Submit a Preprint Cite Share Download PDF Research Article A Continuation-Based Solution of the Linearity Challenge Luca Padovani, Claudia Raffaelli This is a preprint; it has not been peer reviewed by a journal. https://doi.org/ 10.21203/rs.3.rs-8499890/v1 This work is licensed under a CC BY 4.0 License Status: Under Revision Version 1 posted 9 You are reading this latest preprint version Abstract The formalisation of session calculi is made difficult by the management of session channels, which are linear resources that cannot be discarded or duplicated and whose type changes over time, as input/output operations are performed on them. Context splitting, the channel management technique directly related to the way session type theories are usually written with pen and paper, is often considered a hindrance and a notable source of complexity, to the point where several alternative approaches have been recently proposed. In this paper we describe the Agda formalisation of a process calculus based on classical linear logic that supports the modeling of binary sessions through their encoding with explicit continuation channels. The formalisation turns out to be remarkably compact despite the adoption of context splitting. We argue that the logical nature of the calculus and the use of explicit continuations are contributing factors to the simplicity of its formalisation. session types linear logic continuations deadlock freedom Agda Full Text Additional Declarations No competing interests reported. Cite Share Download PDF Status: Under Revision Version 1 posted Editorial decision: Revision requested 15 Apr, 2026 Reviews received at journal 14 Apr, 2026 Reviews received at journal 15 Mar, 2026 Reviewers agreed at journal 02 Mar, 2026 Reviewers agreed at journal 29 Jan, 2026 Reviewers invited by journal 19 Jan, 2026 Editor assigned by journal 05 Jan, 2026 Submission checks completed at journal 05 Jan, 2026 First submitted to journal 02 Jan, 2026 You are reading this latest preprint version Research Square lets you share your work early, gain feedback from the community, and start making changes to your manuscript prior to peer review in a journal. As a division of Research Square Company, we’re committed to making research communication faster, fairer, and more useful. We do this by developing innovative software and high quality services for the global research community. Our growing team is made up of researchers and industry professionals working together to solve the most critical problems facing scientific publishing. Also discoverable on Platform About Our Team In Review Editorial Policies Advisory Board Help Center Resources Author Services Accessibility API Access RSS feed Manage Cookie Preferences © Research Square 2026 | ISSN 2693-5015 (online) Privacy Policy Terms of Service Do Not Sell My Personal Information {"props":{"pageProps":{"initialData":{"identity":"rs-8499890","acceptedTermsAndConditions":true,"allowDirectSubmit":false,"archivedVersions":[],"articleType":"Research Article","associatedPublications":[],"authors":[{"id":577587582,"identity":"4b25ce1c-e852-4e87-907a-e7ac0ead4241","order_by":0,"name":"Luca Padovani","email":"data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAZAAAAAyAQMAAABI0h/eAAAABlBMVEX///8AAABVwtN+AAAACXBIWXMAAA7EAAAOxAGVKw4bAAAA8klEQVRIiWNgGAWjYBACPijN2AAiEypsGBiYeYAsA9xa2FC1nEmDacGtB1ULY9thIAnSgscaNonkhx8Yd9jJ9kskP3vwgO184nZ23oMPGAr+4NGSZizBeCbZeOaMNHODBJ7biTub+ZIN8DpMIodBgrGNOXHDmQNmEgkStxM3HOYxkyCghfkHY1s9UMvxbxIJBueI0sIGtOVw4objPUBbEg4QoYXnmZlF4pnjxjPbe8okEg4kG284DPRLgoExTi387MmPb3zcUS3bz8y+TfLnPzvZDefPHnzw4Y8cTi1gkNiALpKAXwMsHkfBKBgFo2AU4AAApsNPwEqwf1MAAAAASUVORK5CYII=","orcid":"","institution":"University of Bologna","correspondingAuthor":true,"prefix":"","firstName":"Luca","middleName":"","lastName":"Padovani","suffix":""},{"id":577587585,"identity":"522c9673-0fd8-4894-863c-1974183dfcff","order_by":1,"name":"Claudia Raffaelli","email":"","orcid":"","institution":"University of Camerino","correspondingAuthor":false,"prefix":"","firstName":"Claudia","middleName":"","lastName":"Raffaelli","suffix":""}],"badges":[],"createdAt":"2026-01-02 10:08:17","currentVersionCode":1,"declarations":"","doi":"10.21203/rs.3.rs-8499890/v1","doiUrl":"https://doi.org/10.21203/rs.3.rs-8499890/v1","draftVersion":[],"editorialEvents":[],"editorialNote":"","failedWorkflow":false,"files":[{"id":100780805,"identity":"655f389d-2695-4c56-8efa-82a53d6335da","added_by":"auto","created_at":"2026-01-21 11:41:37","extension":"json","order_by":0,"title":"","display":"","copyAsset":false,"role":"acdc-reference","size":3624,"visible":true,"origin":"","legend":"","description":"","filename":"5263e630c9c8442a86a194b74981df71.json","url":"https://assets-eu.researchsquare.com/files/rs-8499890/v1/1dbfca272fc83d5cb0d44fca.json"},{"id":100785432,"identity":"62b15604-f037-4566-9449-9a942f6ed484","added_by":"auto","created_at":"2026-01-21 11:55:51","extension":"pdf","order_by":1,"title":"","display":"","copyAsset":false,"role":"manuscript-pdf","size":418477,"visible":true,"origin":"","legend":"","description":"","filename":"archive.pdf","url":"https://assets-eu.researchsquare.com/files/rs-8499890/v1_covered_4e802f46-98a5-490b-93cf-c2dc960dd74d.pdf"}],"financialInterests":"No competing interests reported.","formattedTitle":"A Continuation-Based Solution of the Linearity Challenge","fulltext":[],"fulltextSource":"","fullText":"","funders":[],"hasAdminPriorityOnWorkflow":false,"hasManuscriptDocX":false,"hasOptedInToPreprint":true,"hasPassedJournalQc":"","hasAnyPriority":false,"hideJournal":false,"highlight":"","institution":"","isAcceptedByJournal":false,"isAuthorSuppliedPdf":true,"isDeskRejected":"","isHiddenFromSearch":false,"isInQc":false,"isInWorkflow":false,"isPdf":true,"isPdfUpToDate":true,"isWithdrawnOrRetracted":false,"journal":{"display":true,"email":"[email protected]","identity":"journal-of-automated-reasoning","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":false,"externalIdentity":"jars","sideBox":"Learn more about [Journal of Automated Reasoning](http://link.springer.com/journal/10817)","snPcode":"10817","submissionUrl":"https://submission.nature.com/new-submission/10817/3","title":"Journal of Automated Reasoning","twitterHandle":"","acdcEnabled":true,"dfaEnabled":true,"editorialSystem":"em","reportingPortfolio":"Springer Hybrid","inReviewEnabled":true,"inReviewRevisionsEnabled":false},"keywords":"session types, linear logic, continuations, deadlock freedom, Agda","lastPublishedDoi":"10.21203/rs.3.rs-8499890/v1","lastPublishedDoiUrl":"https://doi.org/10.21203/rs.3.rs-8499890/v1","license":{"name":"CC BY 4.0","url":"https://creativecommons.org/licenses/by/4.0/"},"manuscriptAbstract":"The formalisation of session calculi is made difficult by the management of session channels, which are linear resources that cannot be discarded or duplicated and whose type changes over time, as input/output operations are performed on them. Context splitting, the channel management technique directly related to the way session type theories are usually written with pen and paper, is often considered a hindrance and a notable source of complexity, to the point where several alternative approaches have been recently proposed. In this paper we describe the Agda formalisation of a process calculus based on classical linear logic that supports the modeling of binary sessions through their encoding with explicit continuation channels. The formalisation turns out to be remarkably compact despite the adoption of context splitting. We argue that the logical nature of the calculus and the use of explicit continuations are contributing factors to the simplicity of its formalisation.","manuscriptTitle":"A Continuation-Based Solution of the Linearity Challenge","msid":"","msnumber":"","nonDraftVersions":[{"code":1,"date":"2026-01-21 10:20:19","doi":"10.21203/rs.3.rs-8499890/v1","editorialEvents":[{"type":"communityComments","content":0},{"type":"decision","content":"Revision requested","date":"2026-04-15T16:42:47+00:00","index":"","fulltext":""},{"type":"editorInvitedReview","content":"","date":"2026-04-14T15:28:17+00:00","index":"hide","fulltext":""},{"type":"editorInvitedReview","content":"","date":"2026-03-15T06:34:35+00:00","index":"hide","fulltext":""},{"type":"reviewerAgreed","content":"105146236159373952747174973984915837082","date":"2026-03-02T19:47:35+00:00","index":"hide","fulltext":""},{"type":"reviewerAgreed","content":"253668048990693499500006256085050304624","date":"2026-01-29T09:09:33+00:00","index":"hide","fulltext":""},{"type":"reviewersInvited","content":"","date":"2026-01-20T01:51:51+00:00","index":"","fulltext":""},{"type":"editorAssigned","content":"","date":"2026-01-05T07:17:51+00:00","index":"","fulltext":""},{"type":"checksComplete","content":"","date":"2026-01-05T07:17:43+00:00","index":"","fulltext":""},{"type":"submitted","content":"Journal of Automated Reasoning","date":"2026-01-02T09:56:28+00:00","index":"","fulltext":""}],"status":"published","journal":{"display":true,"email":"[email protected]","identity":"journal-of-automated-reasoning","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":false,"externalIdentity":"jars","sideBox":"Learn more about [Journal of Automated Reasoning](http://link.springer.com/journal/10817)","snPcode":"10817","submissionUrl":"https://submission.nature.com/new-submission/10817/3","title":"Journal of Automated Reasoning","twitterHandle":"","acdcEnabled":true,"dfaEnabled":true,"editorialSystem":"em","reportingPortfolio":"Springer Hybrid","inReviewEnabled":true,"inReviewRevisionsEnabled":false}}],"origin":"","ownerIdentity":"4184deec-fdf2-4622-b99b-c4844630a995","owner":[],"postedDate":"January 21st, 2026","published":true,"recentEditorialEvents":[],"rejectedJournal":[],"revision":"","amendment":"","status":"in-revision","subjectAreas":[],"tags":[],"updatedAt":"2026-04-15T16:55:16+00:00","versionOfRecord":[],"versionCreatedAt":"2026-01-21 10:20:19","video":"","vorDoi":"","vorDoiUrl":"","workflowStages":[]},"version":"v1","identity":"rs-8499890","journalConfig":"researchsquare"},"__N_SSP":true},"page":"/article/[identity]/[[...version]]","query":{"redirect":"/article/rs-8499890","identity":"rs-8499890","version":["v1"]},"buildId":"XKTyCvWXoU3ODBz1xrDgd","isFallback":false,"isExperimentalCompile":false,"dynamicIds":[84888],"gssp":true,"scriptLoader":[]}