{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T18:55:04Z","timestamp":1784314504151,"version":"3.55.0"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,5,18]],"date-time":"2024-05-18T00:00:00Z","timestamp":1715990400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,5,18]],"date-time":"2024-05-18T00:00:00Z","timestamp":1715990400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["2425191"],"award-info":[{"award-number":["2425191"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a formal framework for process composition based on actions that are specified by their input and output resources. The correctness of these compositions is verified by translating them into deductions in intuitionistic linear logic. As part of the verification we derive simple conditions on the compositions which ensure well-formedness of the corresponding deduction when satisfied. We mechanise the whole framework, including a deep embedding of ILL, in the proof assistant Isabelle\/HOL. Beyond the increased confidence in our proofs, this allows us to automatically generate executable code for our verified definitions. We demonstrate our approach by formalising part of the simulation game Factorio and modelling a manufacturing process in it. Our framework guarantees that this model is free of bottlenecks.<\/jats:p>","DOI":"10.1007\/s10817-024-09698-2","type":"journal-article","created":{"date-parts":[[2024,5,18]],"date-time":"2024-05-18T02:01:29Z","timestamp":1715997689000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Linear Resources in Isabelle\/HOL"],"prefix":"10.1007","volume":"68","author":[{"given":"Filip","family":"Smola","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jacques D.","family":"Fleuriot","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,5,18]]},"reference":[{"issue":"1","key":"9698_CR1","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/0304-3975(94)00103-0","volume":"135","author":"S Abramsky","year":"1994","unstructured":"Abramsky, S.: Proofs as processes. Theor. Comput. Sci. 135(1), 5\u20139 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)00103-0","journal-title":"Theor. Comput. Sci."},{"key":"9698_CR2","unstructured":"Barber, A.G.: Dual intuitionistic linear logic. Technical Report ECS-LFCS-96-347, University of Edinburgh (1996)"},{"issue":"1","key":"9698_CR3","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/0304-3975(94)00104-9","volume":"135","author":"G Bellin","year":"1994","unstructured":"Bellin, G., Scott, P.J.: On the $$\\pi $$-calculus and linear logic. Theor. Comput. Sci. 135(1), 11\u201365 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)00104-9","journal-title":"Theor. Comput. Sci."},{"key":"9698_CR4","doi-asserted-by":"publisher","unstructured":"Bierman, G.M.: On intuitionistic linear logic. Technical Report UCAM-CL-TR-346. University of Cambridge, Computer Laboratory (August 1994). https:\/\/doi.org\/10.48456\/tr-346","DOI":"10.48456\/tr-346"},{"key":"9698_CR5","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-642-24364-6_2","volume-title":"Frontiers of Combining Systems","author":"JC Blanchette","year":"2011","unstructured":"Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle\/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) Frontiers of Combining Systems, pp. 12\u201327. Springer, Berlin (2011)"},{"key":"9698_CR6","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-08970-6_7","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving, pp. 93\u2013110. Springer, Cham (2014)"},{"key":"9698_CR7","unstructured":"Boardman, B.S., Krejci, C.C.: Simulation of production and inventory control using the computer game factorio. In: ASEE 2021 Gulf-Southwest Annual Conference (2021)"},{"key":"9698_CR8","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-642-15375-4_16","volume-title":"CONCUR 2010\u2014Concurrency Theory","author":"L Caires","year":"2010","unstructured":"Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010\u2014Concurrency Theory, pp. 222\u2013236. Springer, Berlin (2010)"},{"key":"9698_CR9","volume-title":"Universal Algebra","author":"PM Cohn","year":"1965","unstructured":"Cohn, P.M.: Universal Algebra. Harper & Row, New York (1965)"},{"key":"9698_CR10","volume-title":"A Discipline of Mathematical Systems Modelling. Systems thinking and systems engineering","author":"M Collinson","year":"2012","unstructured":"Collinson, M., Monahan, B., Pym, D.: A Discipline of Mathematical Systems Modelling. Systems thinking and systems engineering. College Publications, London (2012)"},{"key":"9698_CR11","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-16242-8_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"JE Dawson","year":"2010","unstructured":"Dawson, J.E., Gor\u00e9, R.: Generic methods for formalising sequent calculi applied to provability logic. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, pp. 263\u2013277. Springer, Berlin (2010)"},{"key":"9698_CR12","unstructured":"Dixon, L., Smaill, A., Bundy, A.: Verified planning by deductive synthesis in intuitionistic linear logic. In: Workshop on Verification and Validation of Planning and Scheduling Systems: ICALP 2009 (2009)"},{"key":"9698_CR13","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-030-51054-1_4","volume-title":"Automated Reasoning","author":"B F\u00fcrer","year":"2020","unstructured":"F\u00fcrer, B., Lochbihler, A., Schneider, J., Traytel, D.: Quotients of bounded natural functors. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning, pp. 58\u201378. Springer, Cham (2020)"},{"issue":"1","key":"9698_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J-Y Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50(1), 1\u2013101 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"9698_CR15","unstructured":"Haftmann, F.: Code Generation from Isabelle Theories. https:\/\/isabelle.in.tum.de\/doc\/codegen.pdf"},{"key":"9698_CR16","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: Hol light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, pp. 60\u201366. Springer, Berlin (2009)"},{"issue":"2","key":"9698_CR17","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1006\/inco.1994.1036","volume":"110","author":"JS Hodas","year":"1994","unstructured":"Hodas, J.S., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Inf. Comput. 110(2), 327\u2013365 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1036","journal-title":"Inf. Comput."},{"key":"9698_CR18","first-page":"509","volume-title":"CONCUR\u201993","author":"K Honda","year":"1993","unstructured":"Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR\u201993, pp. 509\u2013523. Springer, Berlin (1993)"},{"key":"9698_CR19","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-03545-1_9","volume-title":"Certified Programs and Proofs","author":"B Huffman","year":"2013","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) Certified Programs and Proofs, pp. 131\u2013146. Springer, Cham (2013)"},{"key":"9698_CR20","doi-asserted-by":"publisher","unstructured":"Ierusalimschy, R., Figueiredo, L.H., Filho, W.C.: Lua-an extensible extension language. Software: Practice and Experience 26(6), 635\u2013652 (1996) https:\/\/doi.org\/10.1002\/(SICI)1097-024X(199606)26:6<635::AID-SPE26>3.0.CO;2-P","DOI":"10.1002\/(SICI)1097-024X(199606)26:6<635::AID-SPE26>3.0.CO;2-P"},{"key":"9698_CR21","unstructured":"Kalvala, S., De\u00a0Paiva, V.: Mechanizing linear logic in Isabelle. In: In 10th International Congress of Logic, Philosophy and Methodology of Science, vol. 24. Citeseer (1995)"},{"key":"9698_CR22","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-25932-9_14","volume-title":"Declarative Agent Languages and Technologies","author":"P K\u00fcngas","year":"2004","unstructured":"K\u00fcngas, P., Matskin, M.: Linear logic, partial deduction and cooperative problem solving. In: Leite, J., Omicini, A., Sterling, L., Torroni, P. (eds.) Declarative Agent Languages and Technologies, pp. 263\u2013279. Springer, Berlin (2004)"},{"key":"9698_CR23","unstructured":"Leroy, X., Doligez, D., Frisch, A., Garrigue, J., R\u00e9my, D., Vouillon, J.: The Objective Caml System\u2014Documentation and User\u2019s Manual. http:\/\/caml.inria.fr\/pub\/docs\/manual-ocaml\/"},{"issue":"4","key":"9698_CR24","doi-asserted-by":"publisher","first-page":"1156","DOI":"10.1109\/JBHI.2016.2579881","volume":"21","author":"A Manataki","year":"2017","unstructured":"Manataki, A., Fleuriot, J., Papapanagiotou, P.: A workflow-driven formal methods approach to the generation of structured checklists for intrahospital patient transfers. IEEE J. Biomed. Health Inform. 21(4), 1156\u20131162 (2017). https:\/\/doi.org\/10.1109\/JBHI.2016.2579881","journal-title":"IEEE J. Biomed. Health Inform."},{"key":"9698_CR25","unstructured":"McCarthy, J., Hayes, P.J.: Some philosophical problems from the standpoint of artificial intelligence. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 4, pp. 463\u2013502. Edinburgh University Press, Edinburgh (1969). reprinted in McC90"},{"key":"9698_CR26","doi-asserted-by":"publisher","unstructured":"Miller, D.: A multiple-conclusion meta-logic. In: Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp. 272\u2013281 (1994). https:\/\/doi.org\/10.1109\/LICS.1994.316062","DOI":"10.1109\/LICS.1994.316062"},{"key":"9698_CR27","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-58041-3_6","volume-title":"Logic and Algebra of Specification","author":"R Milner","year":"1993","unstructured":"Milner, R.: The polyadic $$\\pi $$-calculus: a tutorial. In: Bauer, F.L., Brauer, W., Schwichtenberg, H. (eds.) Logic and Algebra of Specification, pp. 203\u2013246. Springer, Berlin (1993)"},{"key":"9698_CR28","volume-title":"The Definition of Standard ML","author":"R Milner","year":"1990","unstructured":"Milner, R., Toft, M., Harper, R.: The Definition of Standard ML. MIT, Cambridge (1990)"},{"issue":"4","key":"9698_CR29","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541\u2013580 (1989). https:\/\/doi.org\/10.1109\/5.24143","journal-title":"Proc. IEEE"},{"key":"9698_CR30","volume-title":"An Overview of the Scala Programming Language","author":"M Odersky","year":"2004","unstructured":"Odersky, M., Altherr, P., Cremet, V., Emir, B., Maneth, S., Micheloud, S., Mihaylov, N., Schinz, M., Stenman, E., Zenger, M.: An Overview of the Scala Programming Language. EPFL, Lausanne (2004)"},{"issue":"2","key":"9698_CR31","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"PW O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bull. Symb. Logic 5(2), 215\u2013244 (1999). https:\/\/doi.org\/10.2307\/421090","journal-title":"Bull. Symb. Logic"},{"key":"9698_CR32","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-319-15895-2_3","volume-title":"Business Process Management Workshops","author":"P Papapanagiotou","year":"2015","unstructured":"Papapanagiotou, P., Fleuriot, J.: Modelling and implementation of correct by construction healthcare workflows. In: Fournier, F., Mendling, J. (eds.) Business Process Management Workshops, pp. 28\u201339. Springer, Cham (2015)"},{"key":"9698_CR33","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-319-63046-5_22","volume-title":"Automated Deduction\u2014CADE 26","author":"P Papapanagiotou","year":"2017","unstructured":"Papapanagiotou, P., Fleuriot, J.: WorkflowFM: a logic-based framework for formal process specification and composition. In: Moura, L. (ed.) Automated Deduction\u2014CADE 26, pp. 357\u2013370. Springer, Cham (2017)"},{"key":"9698_CR34","doi-asserted-by":"publisher","unstructured":"Papapanagiotou, P., Vaughan, J., Smola, F., Fleuriot, J.: A real-world case study of process and data driven predictive analytics for manufacturing workflows. In: Proceedings of the 54th Hawaii International Conference on System Sciences 2021, HICSS-54, pp. 1001\u20131010, 05-01-2021\u201308-01-2021 (2021). https:\/\/doi.org\/10.24251\/HICSS.2021.122","DOI":"10.24251\/HICSS.2021.122"},{"key":"9698_CR35","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Isabelle A Generic Theorem Prover, 1st edn. Lecture Notes in Computer Science, vol. 828. Springer, Berlin (1994)","DOI":"10.1007\/BFb0030541"},{"key":"9698_CR36","doi-asserted-by":"crossref","unstructured":"Peyton-Jones, S.: The Haskell 98 language and libraries: the revised report. J. Funct. Program. 13(l), i\u2013xii, l-255 (2003)","DOI":"10.1017\/S0956796803003010"},{"key":"9698_CR37","unstructured":"Power, J.F., Webster, C.: Working with linear logic in Coq. In: 12th International Conference on Theorem Proving in Higher Order Logics, pp. 1\u201316 (1999). This is the Work-in-progress version of the paper. https:\/\/mural.maynoothuniversity.ie\/6461\/"},{"key":"9698_CR38","doi-asserted-by":"publisher","unstructured":"Pym, D.J., O\u2019Hearn, P.W., Yang, H.: Possible worlds and resources: the semantics of bi. Theor. Comput. Sci. 315(1), 257\u2013305 (2004). https:\/\/doi.org\/10.1016\/j.tcs.2003.11.020. Mathematical Foundations of Programming Semantics","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"9698_CR39","doi-asserted-by":"publisher","unstructured":"Reid, K.N., Miralavy, I., Kelly, S., Banzhaf, W., Gondro, C.: The factory must grow: automation in factorio. In: Proceedings of the Genetic and Evolutionary Computation Conference Companion. GECCO \u201921, pp. 243\u2013244. Association for Computing Machinery, New York (2021). https:\/\/doi.org\/10.1145\/3449726.3459463","DOI":"10.1145\/3449726.3459463"},{"key":"9698_CR40","unstructured":"Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach. Pearson Custom Library. Pearson Education, Harlow (2013)"},{"key":"9698_CR41","unstructured":"Sternagel, C., Thiemann, R.: Abstract rewriting. Archive of Formal Proofs. Formal proof development (2010). http:\/\/isa-afp.org\/entries\/Abstract-Rewriting.html"},{"key":"9698_CR42","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-642-03359-9_31","volume-title":"Theorem Proving in Higher Order Logics","author":"R Thiemann","year":"2009","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, pp. 452\u2013468. Springer, Berlin (2009)"},{"key":"9698_CR43","doi-asserted-by":"crossref","unstructured":"Traytel, D., Popescu, A., Blanchette, J.C.: Foundational, compositional (co) datatypes for higher-order logic: category theory applied to theorem proving. In: 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp. 596\u2013605. IEEE (2012)","DOI":"10.1109\/LICS.2012.75"},{"key":"9698_CR44","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Propositions as sessions. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming. ICFP \u201912, pp. 273\u2013286. Association for Computing Machinery, New York (2012). https:\/\/doi.org\/10.1145\/2364527.2364568","DOI":"10.1145\/2364527.2364568"},{"issue":"12","key":"9698_CR45","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/2699407","volume":"58","author":"P Wadler","year":"2015","unstructured":"Wadler, P.: Propositions as types. Commun. ACM 58(12), 75\u201384 (2015). https:\/\/doi.org\/10.1145\/2699407","journal-title":"Commun. ACM"},{"key":"9698_CR46","unstructured":"Wenzel, M.: Isabelle\/Isar\u2014a generic framework for human-readable proof documents. Stud. Log. Gramm. Rhetor. 10(23), 277\u2013298 (2007). From Insight to Proof\u2014Festschrift in Honour of Andrzej Trybulec"},{"key":"9698_CR47","doi-asserted-by":"publisher","unstructured":"Xavier, B., Olarte, C., Reis, G., Nigam, V.: Mechanizing focused linear logic in Coq. Electronic Notes in Theoretical Computer Science 338, 219\u2013236 (2018) https:\/\/doi.org\/10.1016\/j.entcs.2018.10.014 . The 12th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2017)","DOI":"10.1016\/j.entcs.2018.10.014"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09698-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09698-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09698-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,22]],"date-time":"2024-06-22T07:08:00Z","timestamp":1719040080000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09698-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,18]]},"references-count":47,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["9698"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09698-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,5,18]]},"assertion":[{"value":"23 August 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 April 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 May 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have not disclosed any competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"9"}}