{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T15:52:46Z","timestamp":1787068366713,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030684457","type":"print"},{"value":"9783030684464","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,2,13]],"date-time":"2021-02-13T00:00:00Z","timestamp":1613174400000},"content-version":"vor","delay-in-days":43,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Linear types provide a way to constrain programs by specifying that some values must be used exactly once. Recent work on\n                    <jats:italic>graded modal types<\/jats:italic>\n                    augments and refines this notion, enabling fine-grained, quantitative specification of data use in programs. The information provided by graded modal types appears to be useful for type-directed program synthesis, where these additional constraints can be used to prune the search space of candidate programs. We explore one of the major implementation challenges of a synthesis algorithm in this setting: how does the synthesis algorithm efficiently ensure that resource constraints are satisfied throughout program generation? We provide two solutions to this\n                    <jats:italic>resource management<\/jats:italic>\n                    problem, adapting Hodas and Miller\u2019s input-output model of linear context management to a graded modal linear type theory. We evaluate the performance of both approaches via their implementation as a program synthesis tool for the programming language Granule, which provides linear and graded modal typing.\n                  <\/jats:p>","DOI":"10.1007\/978-3-030-68446-4_8","type":"book-chapter","created":{"date-parts":[[2021,2,12]],"date-time":"2021-02-12T14:06:39Z","timestamp":1613138799000},"page":"151-170","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Resourceful Program Synthesis from Graded Linear Types"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3174-4689","authenticated-orcid":false,"given":"Jack","family":"Hughes","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7058-7842","authenticated-orcid":false,"given":"Dominic","family":"Orchard","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,2,13]]},"reference":[{"key":"8_CR1","unstructured":"Logic programming with linear logic. http:\/\/www.cs.rmit.edu.au\/lygon\/, Accessed 19 June 2020"},{"key":"8_CR2","unstructured":"Allais, G.: Typing with leftovers-a mechanization of intuitionistic multiplicative-additive linear logic. In: 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2018)"},{"issue":"3","key":"8_CR3","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"JM Andreoli","year":"1992","unstructured":"Andreoli, J.M.: Logic programming with focusing proofs in linear logic. J. Logic Comput. 2(3), 297\u2013347 (1992). https:\/\/doi.org\/10.1093\/logcom\/2.3.297","journal-title":"J. Logic Comput."},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-54833-8_19","volume-title":"Programming Languages and Systems","author":"A Brunel","year":"2014","unstructured":"Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A core quantitative coeffect calculus. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 351\u2013370. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_19"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Bucciarelli, A., Kesner, D., Rocca, S.R.D.: Inhabitation for non-idempotent intersection types. Log. Methods Comput. Sci. 14(3) (2018). https:\/\/doi.org\/10.23638\/LMCS-14(3:7)2018","DOI":"10.23638\/LMCS-14"},{"issue":"4","key":"8_CR6","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1093\/jigpal\/jzx018","volume":"25","author":"A Bucciarelli","year":"2017","unstructured":"Bucciarelli, A., Kesner, D., Ventura, D.: Non-idempotent intersection types for the lambda-calculus. Log. J. IGPL 25(4), 431\u2013464 (2017). https:\/\/doi.org\/10.1093\/jigpal\/jzx018","journal-title":"Log. J. IGPL"},{"issue":"1","key":"8_CR7","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00173-5","volume":"232","author":"I Cervesato","year":"2000","unstructured":"Cervesato, I., Hodas, J.S., Pfenning, F.: Efficient resource management for linear logic proof search. Theor. Comput. Sci. 232(1), 133\u2013163 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(99)00173-5","journal-title":"Theor. Comput. Sci."},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/11532231_6","volume-title":"Automated Deduction \u2013 CADE-20","author":"K Chaudhuri","year":"2005","unstructured":"Chaudhuri, K., Pfenning, F.: A focusing inverse method theorem prover for first-order linear logic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 69\u201383. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11532231_6"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/11538363_15","volume-title":"Computer Science Logic","author":"K Chaudhuri","year":"2005","unstructured":"Chaudhuri, K., Pfenning, F.: Focusing the inverse method for linear logic. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 200\u2013215. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11538363_15"},{"key":"8_CR10","unstructured":"Clarke, H., Liepelt, V.B., Orchard, D.: Scrap your Reprinter (2017). unpublished manuscript"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Degtyarev, A., Voronkov, A.: Chapter 4 - the inverse method. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, North-Holland, Amsterdam, pp. 179\u2013272 (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50006-0","DOI":"10.1016\/B978-044450813-3\/50006-0"},{"issue":"1","key":"8_CR12","doi-asserted-by":"publisher","first-page":"802","DOI":"10.1145\/2914770.2837629","volume":"51","author":"J Frankle","year":"2016","unstructured":"Frankle, J., Osera, P.M., Walker, D., Zdancewic, S.: Example-directed synthesis: a type-theoretic interpretation. ACM SIGPLAN Not. 51(1), 802\u2013815 (2016)","journal-title":"ACM SIGPLAN Not."},{"issue":"1","key":"8_CR13","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1145\/2480359.2429113","volume":"48","author":"M Gaboardi","year":"2013","unstructured":"Gaboardi, M., Haeberlen, A., Hsu, J., Narayan, A., Pierce, B.C.: Linear dependent types for differential privacy. SIGPLAN Not. 48(1), 357\u2013370 (2013). https:\/\/doi.org\/10.1145\/2480359.2429113","journal-title":"SIGPLAN Not."},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Gaboardi, M., Katsumata, S., Orchard, D.A., Breuvart, F., Uustalu, T.: Combining effects and coeffects via grading. In: Garrigue, J., Keller, G., Sumii, E. (eds.) Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, 18\u201322 September 2016, pp. 476\u2013489. ACM (2016). https:\/\/doi.org\/10.1145\/2951913.2951939","DOI":"10.1145\/2951913.2951939"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische schlie\u00dfen. ii. Mathematische Zeitschrift 39, 405\u2013431 (1935)","DOI":"10.1007\/BF01201363"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-642-54833-8_18","volume-title":"Programming Languages and Systems","author":"DR Ghica","year":"2014","unstructured":"Ghica, D.R., Smith, A.I.: Bounded linear types in a resource semiring. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 331\u2013350. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_18"},{"issue":"1","key":"8_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"JY Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50(1), 1\u2013101 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"8_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(92)90386-T","volume":"97","author":"JY Girard","year":"1992","unstructured":"Girard, J.Y., Scedrov, A., Scott, P.J.: Bounded linear logic: a modular approach to polynomial-time computability. Theor. Comput. Sci. 97(1), 1\u201366 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR19","unstructured":"Harland, J., Pym, D.J.: Resource-distribution via boolean constraints. CoRR cs.LO\/0012018 (2000). https:\/\/arxiv.org\/abs\/cs\/0012018"},{"issue":"2","key":"8_CR20","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1006\/inco.1994.1036","volume":"110","author":"J Hodas","year":"1994","unstructured":"Hodas, J., 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":"8_CR21","unstructured":"Howard, W.A.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press (1980)"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Hughes, J., Orchard, D.: Resourceful program synthesis from graded linear types (Appendix) (2020). https:\/\/doi.org\/10.5281\/zenodo.4314644","DOI":"10.5281\/zenodo.4314644"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Hughes, J., Vollmer, M., Orchard, D.: Deriving distributive laws for graded linear types (2020), unpublished manuscript","DOI":"10.4204\/EPTCS.353.6"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Katsumata, S.: Parametric effect monads and semantics of effect systems. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, San Diego, CA, USA, 20\u201321 January 2014, pp. 633\u2013646. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535846","DOI":"10.1145\/2535838.2535846"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-319-89366-2_6","volume-title":"Foundations of Software Science and Computation Structures","author":"S Katsumata","year":"2018","unstructured":"Katsumata, S.: A double category theoretic analysis of graded linear exponential comonads. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 110\u2013127. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_6"},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"Kiselyov, O., Shan, C.c., Friedman, D.P., Sabry, A.: Backtracking, interleaving, and terminating monad transformers: (functional pearl). SIGPLAN Not. 40(9), 192\u2013203 (2005). https:\/\/doi.org\/10.1145\/1090189.1086390","DOI":"10.1145\/1090189.1086390"},{"key":"8_CR27","unstructured":"Knoth, T., Wang, D., Polikarpova, N., Hoffmann, J.: Resource-Guided Program Synthesis. CoRR abs\/1904.07415 (2019). http:\/\/arxiv.org\/abs\/1904.07415"},{"issue":"46","key":"8_CR28","doi-asserted-by":"publisher","first-page":"4747","DOI":"10.1016\/j.tcs.2009.07.041","volume":"410","author":"C Liang","year":"2009","unstructured":"Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theor. Comput. Sci. 410(46), 4747\u20134768 (2009)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"8_CR29","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z Manna","year":"1980","unstructured":"Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. (TOPLAS) 2(1), 90\u2013121 (1980)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"Olarte, C., de Paiva, V., Pimentel, E., Reis, G.: The ILLTP library for intuitionistic linear logic. In: Ehrhard, T., Fern\u00e1ndez, M., de Paiva, V., de Falco, L.T. (eds.) Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK, 7\u20138 July 2018. EPTCS, vol. 292, pp. 118\u2013132 (2018). https:\/\/doi.org\/10.4204\/EPTCS.292.7","DOI":"10.4204\/EPTCS.292.7"},{"key":"8_CR32","doi-asserted-by":"publisher","unstructured":"Orchard, D., Liepelt, V., Eades III, H.E.: Quantitative program reasoning with graded modal types. PACMPL 3(ICFP), 110:1\u2013110:30 (2019). https:\/\/doi.org\/10.1145\/3341714","DOI":"10.1145\/3341714"},{"issue":"6","key":"8_CR33","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/2813885.2738007","volume":"50","author":"PM Osera","year":"2015","unstructured":"Osera, P.M., Zdancewic, S.: Type-and-example-directed program synthesis. SIGPLAN Not. 50(6), 619\u2013630 (2015). https:\/\/doi.org\/10.1145\/2813885.2738007","journal-title":"SIGPLAN Not."},{"key":"8_CR34","unstructured":"Polikarpova, N., Solar-Lezama, A.: Program synthesis from Polymorphic Refinement Types. CoRR abs\/1510.08419 (2015). http:\/\/arxiv.org\/abs\/1510.08419"},{"key":"8_CR35","doi-asserted-by":"publisher","unstructured":"Smith, C., Albarghouthi, A.: Synthesizing differentially private programs. Proc. ACM Program. Lang. 3(ICFP) (2019). https:\/\/doi.org\/10.1145\/3341698","DOI":"10.1145\/3341698"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Zalakain, U., Dardha, O.: Pi with leftovers: a mechanisation in Agda. arXiv preprint arXiv:2005.05902 (2020)","DOI":"10.1007\/978-3-030-78089-0_9"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-68446-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,16]],"date-time":"2022-12-16T21:12:10Z","timestamp":1671225130000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-68446-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030684457","9783030684464"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-68446-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"13 February 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LOPSTR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logic-Based Program Synthesis and Transformation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bologna","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lopstr2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nms.kcl.ac.uk\/maribel.fernandez\/LOPSTR2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","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":"15","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":"48% - 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","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":"4","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)"}},{"value":"In addition, two invited talks are included in the proceedings. Due to the COVID-19 pandemic the conference was held virtually.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}