{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T12:49:12Z","timestamp":1790945352900,"version":"4.1.0"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572616","type":"print"},{"value":"9783031572623","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Graded type systems are a class of type system for fine-grained quantitative reasoning about data-flow in programs. Through the use of resource annotations (or <jats:italic>grades<\/jats:italic>), a programmer can express various program properties at the type level, reducing the number of typeable programs. These additional constraints on types lend themselves naturally to type-directed <jats:italic>program synthesis<\/jats:italic>, where this information can be exploited to constrain the search space of programs. We present a synthesis algorithm for a graded type system, where grades form an arbitrary pre-ordered semiring. Harnessing this grade information in synthesis is non-trivial, and we explore some of the issues involved in designing and implementing a resource-aware program synthesis tool. In our evaluation we show that by harnessing grades in synthesis, the majority of our benchmark programs (many of which involve recursive functions over recursive ADTs) require less exploration of the synthesis search space than a purely type-driven approach and with fewer needed input-output examples. This <jats:italic>type-and-graded-directed<\/jats:italic> approach is demonstrated for the research language Granule but we also adapt it for synthesising Haskell programs that use GHC\u2019s linear types extension.\n<\/jats:p>","DOI":"10.1007\/978-3-031-57262-3_4","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:02:35Z","timestamp":1712214155000},"page":"83-112","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Program Synthesis from Graded 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":[[2024,4,5]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Abel, A., Bernardy, J.: A unified view of modalities in type systems. Proc. ACM Program. Lang. 4(ICFP), 90:1\u201390:28 (2020). https:\/\/doi.org\/10.1145\/3408972, https:\/\/doi.org\/10.1145\/3408972","DOI":"10.1145\/3408972 10.1145\/3408972"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive program synthesis. In: Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. pp. 934\u2013950 (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_67, https:\/\/doi.org\/10.1007\/978-3-642-39799-8_67","DOI":"10.1007\/978-3-642-39799-8_67 10.1007\/978-3-642-39799-8_67"},{"key":"4_CR3","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)"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Andreoli, J.M.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2(3), 297\u2013347 (06 1992). https:\/\/doi.org\/10.1093\/logcom\/2.3.297","DOI":"10.1093\/logcom\/2.3.297"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Atkey, R.: Syntax and Semantics of Quantitative Type Theory. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 56\u201365 (2018). https:\/\/doi.org\/10.1145\/3209108.3209189, https:\/\/doi.org\/10.1145\/3209108.3209189","DOI":"10.1145\/3209108.3209189 10.1145\/3209108.3209189"},{"key":"4_CR6","unstructured":"Austin, J., Odena, A., Nye, M.I., Bosma, M., Michalewski, H., Dohan, D., Jiang, E., Cai, C.J., Terry, M., Le, Q.V., Sutton, C.: Program synthesis with large language models. CoRR abs\/2108.07732 (2021), https:\/\/arxiv.org\/abs\/2108.07732"},{"key":"4_CR7","unstructured":"Barrett, C., Stump, A., Tinelli, C., et\u00a0al.: The smt-lib standard: Version 2.0. In: Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK). vol.\u00a013, p.\u00a014 (2010)"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Bernardy, J., Boespflug, M., Newton, R.R., Jones, S.P., Spiwack, A.: Linear haskell: practical linearity in a higher-order polymorphic language. Proc. ACM Program. Lang. 2(POPL), 5:1\u20135:29 (2018). https:\/\/doi.org\/10.1145\/3158093, https:\/\/doi.org\/10.1145\/3158093","DOI":"10.1145\/3158093 10.1145\/3158093"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Bove, A., Dybjer, P., Norell, U.: A brief overview of agda\u2013a functional language with dependent types. In: Theorem Proving in Higher Order Logics: 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings 22. pp. 73\u201378. Springer (2009)","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Brady, E.C.: Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program. 23(5), 552\u2013593 (2013). https:\/\/doi.org\/10.1017\/S095679681300018X, https:\/\/doi.org\/10.1017\/S095679681300018X","DOI":"10.1017\/S095679681300018X 10.1017\/S095679681300018X"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Brady, E.C.: Idris 2: Quantitative type theory in practice 194, 9:1\u20139:26 (2021). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2021.9, https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2021.9","DOI":"10.4230\/LIPICS.ECOOP.2021.9 10.4230\/LIPIcs.ECOOP.2021.9"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A core quantitative coeffect calculus. In: Shao, Z. (ed.) Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. Lecture Notes in Computer Science, vol.\u00a08410, pp. 351\u2013370. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_19","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Cervesato, I., Hodas, J.S., Pfenning, F.: Efficient resource management for linear logic proof search. Theoretical Computer Science 232(1), 133 \u2013 163 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(99)00173-5","DOI":"10.1016\/S0304-3975(99)00173-5"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Choudhury, P., III, H.E., Eisenberg, R.A., Weirich, S.: A graded dependent type system with a usage-aware semantics. Proc. ACM Program. Lang. 5(POPL), 1\u201332 (2021). https:\/\/doi.org\/10.1145\/3434331, https:\/\/doi.org\/10.1145\/3434331","DOI":"10.1145\/3434331 10.1145\/3434331"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. SIGPLAN Not. 50(6), 229-239 (jun 2015). https:\/\/doi.org\/10.1145\/2813885.2737977, https:\/\/doi.org\/10.1145\/2813885.2737977","DOI":"10.1145\/2813885.2737977 10.1145\/2813885.2737977"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Fiala, J., Itzhaky, S., M\u00fcller, P., Polikarpova, N., Sergey, I.: Leveraging rust types for program synthesis. Proceedings of the ACM on Programming Languages 7(PLDI), 1414\u20131437 (2023)","DOI":"10.1145\/3591278"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Frankle, J., Osera, P.M., Walker, D., Zdancewic, S.: Example-directed synthesis: a type-theoretic interpretation. ACM SIGPLAN Notices 51(1), 802\u2013815 (2016)","DOI":"10.1145\/2914770.2837629"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Gaboardi, M., Katsumata, S.y., Orchard, D., Breuvart, F., Uustalu, T.: Combining Effects and Coeffects via Grading. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. p. 476-489. ICFP 2016, Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2951913.2951939, https:\/\/doi.org\/10.1145\/2951913.2951939","DOI":"10.1145\/2951913.2951939 10.1145\/2951913.2951939"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"Ghica, D.R., Smith, A.I.: Bounded linear types in a resource semiring. In: Shao, Z. (ed.) Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014. Lecture Notes in Computer Science, vol.\u00a08410, pp. 331\u2013350. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_18","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Girard, J.Y.: Linear logic. Theoretical Computer Science 50(1), 1 \u2013 101 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Girard, J.Y., Scedrov, A., Scott, P.J.: Bounded linear logic: a modular approach to polynomial-time computability. Theoretical computer science 97(1), 1\u201366 (1992)","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Green, C.: Application of theorem proving to problem solving. In: Proceedings of the 1st International Joint Conference on Artificial Intelligence. p. 219-239. IJCAI\u201969, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (1969)","DOI":"10.21236\/ADA459656"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Automating string processing in spreadsheets using input-output examples. ACM Sigplan Notices 46(1), 317\u2013330 (2011)","DOI":"10.1145\/1925844.1926423"},{"key":"4_CR24","unstructured":"Harland, J., Pym, D.J.: Resource-distribution via boolean constraints. CoRR cs.LO\/0012018 (2000), https:\/\/arxiv.org\/abs\/cs\/0012018"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Hodas, J., Miller, D.: Logic Programming in a Fragment of Intuitionistic Linear Logic. Information and Computation 110(2), 327 \u2013 365 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1036","DOI":"10.1006\/inco.1994.1036"},{"key":"4_CR26","unstructured":"Hughes, J., Marshall, D., Wood, J., Orchard, D.: Linear Exponentials as Graded Modal Types. In: 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021). Rome (virtual), Italy (Jun 2021), https:\/\/hal-lirmm.ccsd.cnrs.fr\/lirmm-03271465"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Hughes, J., Orchard, D.: Resourceful program synthesis from graded linear types. In: Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7-9, 2020, Proceedings. pp. 151\u2013170 (2020). https:\/\/doi.org\/10.1007\/978-3-030-68446-4_8, https:\/\/doi.org\/10.1007\/978-3-030-68446-4_8","DOI":"10.1007\/978-3-030-68446-4_8 10.1007\/978-3-030-68446-4_8"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Hughes, J., Orchard, D.: Program Synthesis from Graded Types (Additional Material) (Jan 2024). https:\/\/doi.org\/10.5281\/zenodo.10594378, https:\/\/zenodo.org\/records\/10594378","DOI":"10.5281\/zenodo.10594378"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Hughes, J., Vollmer, M., Orchard, D.: Deriving distributive laws for graded linear types. In: Lago, U.D., de\u00a0Paiva, V. (eds.) Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity &TLLA@IJCAR-FSCD 2020, Online, 29-30 June 2020. EPTCS, vol.\u00a0353, pp. 109\u2013131 (2020). https:\/\/doi.org\/10.4204\/EPTCS.353.6, https:\/\/doi.org\/10.4204\/EPTCS.353.6","DOI":"10.4204\/EPTCS.353.6 10.4204\/EPTCS.353.6"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Jain, N., Vaidyanath, S., Iyer, A., Natarajan, N., Parthasarathy, S., Rajamani, S., Sharma, R.: Jigsaw: Large language models meet program synthesis (2021)","DOI":"10.1145\/3510003.3510203"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Jung, R., Dang, H.H., Kang, J., Dreyer, D.: Stacked borrows: An aliasing model for rust. Proceedings of the ACM on Programming Languages 4(POPL), 1\u201332 (2019)","DOI":"10.1145\/3371109"},{"key":"4_CR32","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, January 20-21, 2014. pp. 633\u2013646. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535846","DOI":"10.1145\/2535838.2535846"},{"key":"4_CR33","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-203 (Sep 2005). https:\/\/doi.org\/10.1145\/1090189.1086390","DOI":"10.1145\/1090189.1086390"},{"key":"4_CR34","doi-asserted-by":"publisher","unstructured":"Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. p. 407-426. OOPSLA \u201913, Association for Computing Machinery, New York, NY, USA (2013). https:\/\/doi.org\/10.1145\/2509136.2509555, https:\/\/doi.org\/10.1145\/2509136.2509555","DOI":"10.1145\/2509136.2509555 10.1145\/2509136.2509555"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Knoth, T., Wang, D., Polikarpova, N., Hoffmann, J.: Resource-Guided Program Synthesis. CoRR abs\/1904.07415 (2019), http:\/\/arxiv.org\/abs\/1904.07415","DOI":"10.1145\/3314221.3314602"},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"Lubin, J., Collins, N., Omar, C., Chugh, R.: Program sketching with live bidirectional evaluation. Proceedings of the ACM on Programming Languages 4(ICFP), 1\u201329 (2020)","DOI":"10.1145\/3408991"},{"key":"4_CR37","doi-asserted-by":"publisher","unstructured":"Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2, 90\u2013121 (01 1980). https:\/\/doi.org\/10.1145\/357084.357090","DOI":"10.1145\/357084.357090"},{"key":"4_CR38","doi-asserted-by":"publisher","unstructured":"Marshall, D., Vollmer, M., Orchard, D.: Linearity and uniqueness: An entente cordiale. In: Sergey, I. (ed.) Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13240, pp. 346\u2013375. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99336-8_13, https:\/\/doi.org\/10.1007\/978-3-030-99336-8_13","DOI":"10.1007\/978-3-030-99336-8_13 10.1007\/978-3-030-99336-8_13"},{"key":"4_CR39","doi-asserted-by":"publisher","unstructured":"McBride, C.: I Got Plenty o\u2019 Nuttin\u2019, pp. 207\u2013233. Springer International Publishing, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30936-1_12","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"Milner, R.: A theory of type polymorphism in programming. Journal of computer and system sciences 17(3), 348\u2013375 (1978)","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"Miltner, A., Nu\u00f1ez, A.T., Brendel, A., Chaudhuri, S., Dillig, I.: Bottom-up synthesis of recursive functional programs using angelic execution. Proceedings of the ACM on Programming Languages 6(POPL), 1\u201329 (2022)","DOI":"10.1145\/3498682"},{"key":"4_CR42","doi-asserted-by":"publisher","unstructured":"Moon, B., III, H.E., Orchard, D.: Graded Modal Dependent Type Theory. In: Yoshida, N. (ed.) Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12648, pp. 462\u2013490. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_17, https:\/\/doi.org\/10.1007\/978-3-030-72019-3_17","DOI":"10.1007\/978-3-030-72019-3_17 10.1007\/978-3-030-72019-3_17"},{"key":"4_CR43","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient smt solver. vol.\u00a04963, pp. 337\u2013340 (04 2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"4_CR44","unstructured":"Odena, A., Shi, K., Bieber, D., Singh, R., Sutton, C., Dai, H.: Bustle: Bottom-up program synthesis through learning-guided exploration. arXiv preprint arXiv:2007.14381 (2020)"},{"key":"4_CR45","doi-asserted-by":"publisher","unstructured":"Orchard, D., Liepelt, V., 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"},{"key":"4_CR46","unstructured":"Orchard, D.A., Petricek, T., Mycroft, A.: The semantic marriage of monads and effects. CoRR abs\/1401.5391 (2014), http:\/\/arxiv.org\/abs\/1401.5391"},{"key":"4_CR47","doi-asserted-by":"publisher","unstructured":"Osera, P.M., Zdancewic, S.: Type-and-example-directed program synthesis. SIGPLAN Not. 50(6), 619-630 (Jun 2015). https:\/\/doi.org\/10.1145\/2813885.2738007","DOI":"10.1145\/2813885.2738007"},{"key":"4_CR48","unstructured":"Osera, P.M.S.: Program synthesis with types (2015)"},{"key":"4_CR49","doi-asserted-by":"publisher","unstructured":"Petricek, T., Orchard, D., Mycroft, A.: Coeffects: a calculus of context-dependent computation. In: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming. pp. 123\u2013135. ACM (2014). https:\/\/doi.org\/10.1145\/2692915.2628160","DOI":"10.1145\/2692915.2628160"},{"key":"4_CR50","doi-asserted-by":"publisher","unstructured":"Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 522-538. PLDI \u201916, Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2908080.2908093, https:\/\/doi.org\/10.1145\/2908080.2908093","DOI":"10.1145\/2908080.2908093 10.1145\/2908080.2908093"},{"key":"4_CR51","doi-asserted-by":"publisher","unstructured":"Smetsers, S., Barendsen, E., van Eekelen, M., Plasmeijer, R.: Guaranteeing safe destructive updates through a type system with uniqueness information for graphs. In: Schneider, H.J., Ehrig, H. (eds.) Graph Transformations in Computer Science. pp. 358\u2013379. Springer Berlin Heidelberg, Berlin, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-57787-4_23","DOI":"10.1007\/3-540-57787-4_23"},{"key":"4_CR52","doi-asserted-by":"publisher","unstructured":"Smith, C., Albarghouthi, A.: Synthesizing differentially private programs. Proc. ACM Program. Lang. 3(ICFP) (Jul 2019). https:\/\/doi.org\/10.1145\/3341698","DOI":"10.1145\/3341698"},{"key":"4_CR53","doi-asserted-by":"crossref","unstructured":"Yuan, Y., Radhakrishna, A., Samanta, R.: Trace-guided inductive synthesis of recursive functional programs. Proceedings of the ACM on Programming Languages 7(PLDI), 860\u2013883 (2023)","DOI":"10.1145\/3591255"},{"key":"4_CR54","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","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57262-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:03:18Z","timestamp":1712214198000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57262-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572616","9783031572623"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57262-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","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":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/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":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"72","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":"25","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":"1","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":"35% - 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.2","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":"8","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":"The proceedings also contain 4 artifact report that have not been part of the original submission","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)"}}]}}