{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:17Z","timestamp":1775790797544,"version":"3.50.1"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030993351","type":"print"},{"value":"9783030993368","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Mechanisation of programming language research is of growing interest, and the act of mechanising type systems and their metatheory is generally becoming easier as new techniques are invented. However, state-of-the-art techniques mostly rely on <jats:italic>structurality<\/jats:italic> of the type system \u2014 that weakening, contraction, and exchange are admissible and variables can be used unrestrictedly once assumed. Linear logic, and many related subsequent systems, provide motivations for breaking some of these assumptions.<\/jats:p><jats:p>We present a framework for mechanising the metatheory of certain substructural type systems, in a style resembling mechanised metatheory of structural type systems. The framework covers a wide range of simply typed syntaxes with semiring usage annotations, via a metasyntax of typing rules. The metasyntax for the premises of a typing rule is related to bunched logic, featuring both sharing and separating conjunction, roughly corresponding to the additive and multiplicative features of linear logic. We use the uniformity of syntaxes to derive type system-generic renaming, substitution, and a form of linearity checking.<\/jats:p>","DOI":"10.1007\/978-3-030-99336-8_14","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"376-402","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["A Framework for Substructural Type Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8080-3350","authenticated-orcid":false,"given":"James","family":"Wood","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4414-5047","authenticated-orcid":false,"given":"Robert","family":"Atkey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Banerjee, A., Heintze, N., Riecke, J.G.: A Core Calculus of Dependency. In: POPL \u201999, pp. 147\u2013160 (1999)","DOI":"10.1145\/292540.292555"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Abel, A., Bernardy, J.P.: A unified view of modalities in type systems. Proc. ACM Program. Lang. 4(ICFP) (Aug 2020), https:\/\/doi.org\/10.1145\/3408972, URL https:\/\/doi.org\/10.1145\/3408972","DOI":"10.1145\/3408972"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Allais, G., Atkey, R., Chapman, J., McBride, C., McKinna, J.: A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. J. Funct. Program. 31, e22 (2021), https:\/\/doi.org\/10.1017\/S0956796820000076, URL https:\/\/doi.org\/10.1017\/S0956796820000076","DOI":"10.1017\/S0956796820000076"},{"key":"14_CR4","doi-asserted-by":"publisher","unstructured":"Atkey, R.: The syntax and semantics of quantitative type theory. In: LICS \u201918: 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, July 9\u201312, 2018, Oxford, United Kingdom (2018), https:\/\/doi.org\/10.1145\/3209108.3209189","DOI":"10.1145\/3209108.3209189"},{"key":"14_CR5","unstructured":"Atkey, R., Wood, J.: Context constrained computation. In: 3rd Workshop on Type-Driven Development (TyDe \u201918), Extended Abstract (2018)"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Benton, P.: A mixed linear and non-linear logic: Proofs, terms and models. pp. 121\u2013135, Springer-Verlag (1994)","DOI":"10.1007\/BFb0022251"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A Core Quantitative Coeffect Calculus. In: ESOP 2014, pp. 351\u2013370 (2014)","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Curien, P.L., Herbelin, H.: The duality of computation. SIGPLAN Not. 35(9), 233\u2013243 (Sep 2000), ISSN 0362\u20131340, https:\/\/doi.org\/10.1145\/357766.351262, URL https:\/\/doi.org\/10.1145\/357766.351262","DOI":"10.1145\/357766.351262"},{"key":"14_CR9","doi-asserted-by":"publisher","unstructured":"Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp. 193\u2013202 (1999), https:\/\/doi.org\/10.1109\/LICS.1999.782615","DOI":"10.1109\/LICS.1999.782615"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Ghica, D.R., Smith, A.I.: Bounded linear types in a resource semiring. In: ESOP 2014, pp. 331\u2013350 (2014)","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Girard, J.Y.: Linear logic. Theor. Comp. Sci. 50, 1\u2013101 (1987)","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"14_CR12","unstructured":"Herbelin, H.: C\u2019est maintenant qu\u2019on calcule, au c\u0153ur de la dualit\u00e9. Habilitation (2005)"},{"key":"14_CR13","doi-asserted-by":"publisher","unstructured":"Licata, D.R., Shulman, M., Riley, M.: A fibrational framework for substructural and modal logics. In: FSCD 2017, pp. 25:1\u201325:22 (2017), https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2017.25","DOI":"10.4230\/LIPIcs.FSCD.2017.25"},{"key":"14_CR14","unstructured":"Lovas, W., Crary, K.: Structural normalization for classical natural deduction (2006)"},{"key":"14_CR15","unstructured":"McBride, C.: Type-preserving renaming and substitution (2005), URL http:\/\/www.strictlypositive.org\/ren-sub.pdf"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. BULLETIN OF SYMBOLIC LOGIC 5(2), 215\u2013244 (1999)","DOI":"10.2307\/421090"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Orchard, D.A., Liepelt, V., Eades, H.: Quantitative program reasoning with graded modal types. Proceedings of the ACM on Programming Languages 3 (June 2019)","DOI":"10.1145\/3342537"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Petricek, T., Orchard, D.A., Mycroft, A.: Coeffects: a calculus of context-dependent computation. In: ICFP 2014, pp. 123\u2013135 (2014)","DOI":"10.1145\/2692915.2628160"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Reed, J., Pierce, B.C.: Distance makes the types grow stronger. In: Hudak, P., Weirich, S. (eds.) ICFP 2010, pp. 157\u2013168 (2010)","DOI":"10.1145\/1932681.1863568"},{"key":"14_CR20","doi-asserted-by":"publisher","unstructured":"Rouvoet, A., Bach Poulsen, C., Krebbers, R., Visser, E.: Intrinsically-typed definitional interpreters for linear, session-typed languages. In: CPP 2020, pp. 284\u2013298 (2020), ISBN 9781450370974, https:\/\/doi.org\/10.1145\/3372885.3373818","DOI":"10.1145\/3372885.3373818"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Wood, J., Atkey, R.: A linear algebra approach to linear metatheory. arXiv preprint arXiv:2005.02247 (2020)","DOI":"10.4204\/EPTCS.353.10"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Wood, J., Atkey, R.: lamudri\/generic-lr (Jan 2022), https:\/\/doi.org\/10.5281\/zenodo.5920051, URL https:\/\/doi.org\/10.5281\/zenodo.5920051","DOI":"10.5281\/zenodo.5920051"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99336-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T05:08:44Z","timestamp":1731647324000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99336-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030993351","9783030993368"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99336-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"HotCRP","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}