{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T10:02:41Z","timestamp":1742983361093,"version":"3.40.3"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572661"},{"type":"electronic","value":"9783031572678"}],"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>Invertible programming languages specify transformations to be run in two directions, such as compression\/decompression or encryption\/decryption. Two key concepts in invertible programming languages are <jats:italic>partial invertibility<\/jats:italic> and <jats:italic>local invertibility<\/jats:italic>. Partial invertibility lets invertible code be parameterized by the results of non-invertible code, whereas local invertibility requires all code to be invertible. The former allows for more flexible programming, while the latter has connections to domains such as low-energy computing and quantum computing. We find that existing approaches lack a satisfying treatment of partial invertibility, leaving the connection to local invertibility unclear.<\/jats:p><jats:p>In this paper, we identify four core constructs for partially invertible programming, and show how to give them a locally invertible interpretation. We show the expressiveness of the constructs by designing the functional invertible language <jats:sc>Kalpis<\/jats:sc>, and show how to give them a locally invertible semantics using the novel arrow combinator language <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsc {rrArr}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mstyle>\n                      <mml:mi>R<\/mml:mi>\n                      <mml:mi>R<\/mml:mi>\n                    <\/mml:mstyle>\n                    <mml:mi>A<\/mml:mi>\n                    <mml:mstyle>\n                      <mml:mi>R<\/mml:mi>\n                      <mml:mi>R<\/mml:mi>\n                    <\/mml:mstyle>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u2014the key idea is viewing partial invertibility as an invertible effect. By formalizing the two systems and giving <jats:sc>Kalpis<\/jats:sc> semantics by translation to <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsc {rrArr}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mstyle>\n                      <mml:mi>R<\/mml:mi>\n                      <mml:mi>R<\/mml:mi>\n                    <\/mml:mstyle>\n                    <mml:mi>A<\/mml:mi>\n                    <mml:mstyle>\n                      <mml:mi>R<\/mml:mi>\n                      <mml:mi>R<\/mml:mi>\n                    <\/mml:mstyle>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, we reconcile partial and local invertibility, solving an open problem in the field. All formal developments are mechanized in Agda.<\/jats:p>","DOI":"10.1007\/978-3-031-57267-8_3","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T16:02:01Z","timestamp":1712246521000},"page":"59-89","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reconciling Partial and Local Invertibility"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-0847-5373","authenticated-orcid":false,"given":"Anders","family":"\u00c5gren Thun\u00e9","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9747-4899","authenticated-orcid":false,"given":"Kazutaka","family":"Matsuda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7780-630X","authenticated-orcid":false,"given":"Meng","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","unstructured":"Abel, A., Chapman, J.: Normalization by evaluation in the delay monad: A case study for coinduction via copatterns and sized types. In: Levy, P., Krishnaswami, N. (eds.) Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2014, Grenoble, France, 12 April 2014. EPTCS, vol.\u00a0153, pp. 51\u201367 (2014). https:\/\/doi.org\/10.4204\/EPTCS.153.4","DOI":"10.4204\/EPTCS.153.4"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Abramsky, S.: A structural approach to reversible computation. Theor. Comput. Sci. 347(3), 441\u2013464 (2005). https:\/\/doi.org\/10.1016\/j.tcs.2005.07.002","DOI":"10.1016\/j.tcs.2005.07.002"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Almendros-Jim\u00e9nez, J.M., Vidal, G.: Automatic partial inversion of inductively sequential functions. In: Horv\u00e1th, Z., Zs\u00f3k, V., Butterfield, A. (eds.) Implementation and Application of Functional Languages, 18th International Symp osium, IFL 2006, Budapest, Hungary, September 4-6, 2006, Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a04449, pp. 253\u2013270. Springer (2006). https:\/\/doi.org\/10.1007\/978-3-540-74130-5_15","DOI":"10.1007\/978-3-540-74130-5_15"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. J. ACM 47(4), 776\u2013822 (2000). https:\/\/doi.org\/10.1145\/347476.347484","DOI":"10.1145\/347476.347484"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Axelsen, H.B., Gl\u00fcck, R.: What do reversible programs compute? In: Hofmann, M. (ed.) Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06604, pp. 42\u201356. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-19805-2_4","DOI":"10.1007\/978-3-642-19805-2_4"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Axelsen, H.B., Gl\u00fcck, R., Yokoyama, T.: Reversible machine code and its abstract processor architecture. In: Diekert, V., Volkov, M.V., Voronkov, A. (eds.) Computer Science - Theory and Applications, Second International Symposium on Computer Science in Russia, CSR 2007, Ekaterinburg, Russia, September 3-7, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04649, pp. 56\u201369. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-74510-5_9","DOI":"10.1007\/978-3-540-74510-5_9"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Baker, H.G.: NREVERSAL of fortune - the thermodynamics of garbage collection. In: Bekkers, Y., Cohen, J. (eds.) Memory Management, International Workshop IWMM 92, St. Malo, France, September 17-19, 1992, Proceedings. Lecture Notes in Computer Science, vol.\u00a0637, pp. 507\u2013524. Springer (1992). https:\/\/doi.org\/10.1007\/BFb0017210","DOI":"10.1007\/BFb0017210"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Bennett, C.H.: Logical reversibility of computation. IBM Journal of Research and Development 17(6), 525\u2013532 (11 1973). https:\/\/doi.org\/10.1147\/rd.176.0525","DOI":"10.1147\/rd.176.0525"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Bernardy, J., Boespflug, M., Newton, R.R., Peyton Jones, S., Spiwack, A.: Linear haskell: practical linearity in a higher-order polymorphic language. PACMPL 2(POPL), 5:1\u20135:29 (2018). https:\/\/doi.org\/10.1145\/3158093","DOI":"10.1145\/3158093"},{"key":"3_CR10","unstructured":"Bowman, W.J., James, R.P., Sabry, A.: Dagger traced symmetric monoidal categories and reversible programming. Work-in-progress report in the 3rd Workshop on Reversible Computation (July 2011), available from https:\/\/www.williamjbowman.com\/resources\/cat-rev.pdf (visited Jan 23, 2024)"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Capretta, V.: General recursion via coinductive types. Logical Methods in Computer Science 1(2), Article No.\u00a01 (2005). https:\/\/doi.org\/10.2168\/LMCS-1(2:1)2005","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Chen, C., Sabry, A.: A computational interpretation of compact closed categories: reversible programming with negative and fractional types. Proc. ACM Program. Lang. 5(POPL), 1\u201329 (2021). https:\/\/doi.org\/10.1145\/3434290","DOI":"10.1145\/3434290"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Davies, R., Pfenning, F.: A modal analysis of staged computation. J. ACM 48(3), 555\u2013604 (2001). https:\/\/doi.org\/10.1145\/382780.382785","DOI":"10.1145\/382780.382785"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Fischer, S., Kiselyov, O., Shan, C.: Purely functional lazy nondeterministic programming. J. Funct. Program. 21(4-5), 413\u2013465 (2011). https:\/\/doi.org\/10.1017\/S0956796811000189","DOI":"10.1017\/S0956796811000189"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Foster, J.N., Greenwald, M.B., Moore, J.T., Pierce, B.C., Schmitt, A.: Combinators for bi-directional tree transformations: a linguistic approach to the view update problem. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005. pp. 233\u2013246. ACM (2005). https:\/\/doi.org\/10.1145\/1040305.1040325","DOI":"10.1145\/1040305.1040325"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Foster, J.N., Greenwald, M.B., Moore, J.T., Pierce, B.C., Schmitt, A.: Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem. ACM Trans. Program. Lang. Syst. 29(3), Article No.\u00a017 (2007). https:\/\/doi.org\/10.1145\/1232420.1232424","DOI":"10.1145\/1232420.1232424"},{"key":"3_CR17","unstructured":"Frank, M.P.: The R programming language and compiler. MIT Reversible Computing Project Memo #M8, MIT AI Lab (7 1997), available on: https:\/\/github.com\/mikepfrank\/Rlang-compiler\/blob\/master\/docs\/MIT-RCP-MemoM8-RProgLang.pdf"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Gl\u00fcck, R., Kawabe, M.: A program inverter for a functional language with equality and constructors. In: Ohori, A. (ed.) Programming Languages and Systems, First Asian Symposium, APLAS 2003, Beijing, China, November 27-29, 2003, Proceedings. Lecture Notes in Computer Science, vol.\u00a02895, pp. 246\u2013264. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-40018-9_17","DOI":"10.1007\/978-3-540-40018-9_17"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Gl\u00fcck, R., Yokoyama, T.: A linear-time self-interpreter of a reversible imperative language. Computer Software 33(3), 3_108\u20133_128 (2016). https:\/\/doi.org\/10.11309\/jssst.33.3_108","DOI":"10.11309\/jssst.33.3_108"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Goldstein, H., Frohlich, S., Wang, M., Pierce, B.C.: Reflecting on random generation. Proc. ACM Program. Lang. 7(ICFP) (aug 2023). https:\/\/doi.org\/10.1145\/3607842","DOI":"10.1145\/3607842"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Gomard, C.K., Jones, N.D.: A partial evaluator for the untyped lambda-calculus. J. Funct. Program. 1(1), 21\u201369 (1991). https:\/\/doi.org\/10.1017\/S0956796800000058","DOI":"10.1017\/S0956796800000058"},{"key":"3_CR22","doi-asserted-by":"publisher","unstructured":"Heunen, C., Kaarsgaard, R.: Quantum information effects. Proc. ACM Program. Lang. 6(POPL), 1\u201327 (2022). https:\/\/doi.org\/10.1145\/3498663","DOI":"10.1145\/3498663"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Heunen, C., Kaarsgaard, R., Karvonen, M.: Reversible effects as inverse arrows. Electronic Notes in Theoretical Computer Science 341, 179\u2013199 (2018). https:\/\/doi.org\/10.1016\/j.entcs.2018.11.009","DOI":"10.1016\/j.entcs.2018.11.009"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Hughes, J.: Generalising monads to arrows. Sci. Comput. Program. 37(1-3), 67\u2013111 (2000). https:\/\/doi.org\/10.1016\/S0167-6423(99)00023-4","DOI":"10.1016\/S0167-6423(99)00023-4"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"Jacobsen, P.A.H., Kaarsgaard, R., Thomsen, M.K.: $$\\sf CoreFun$$ : A typed functional reversible core language. In: Kari, J., Ulidowski, I. (eds.) Reversible Computation - 10th International Conference, RC 2018, Leicester, UK, September 12-14, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11106, pp. 304\u2013321. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-99498-7_21","DOI":"10.1007\/978-3-319-99498-7_21"},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"James, R.P., Sabry, A.: Information effects. In: Field, J., Hicks, M. (eds.) Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012. pp. 73\u201384. ACM (2012). https:\/\/doi.org\/10.1145\/2103656.2103667","DOI":"10.1145\/2103656.2103667"},{"key":"3_CR27","unstructured":"James, R.P., Sabry, A.: Theseus: a high level language for reversible computing. Work-in-progress report in the 6th Conference on Reversible Computation (2014), available from https:\/\/legacy.cs.indiana.edu\/~sabry\/papers\/theseus.pdf (visited Jan 23, 2024)"},{"key":"3_CR28","unstructured":"Jones, N.D., Gomard, C.K., Sestoft, P.: Partial evaluation and automatic program generation. Prentice Hall international series in computer science, Prentice Hall (1993)"},{"key":"3_CR29","doi-asserted-by":"publisher","unstructured":"Kirkeby, M.H., Gl\u00fcck, R.: Inversion framework: Reasoning about inversion by conditional term rewriting systems. In: PPDP \u201920: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9-10 September, 2020. pp. 9:1\u20139:14. ACM (2020). https:\/\/doi.org\/10.1145\/3414080.3414089","DOI":"10.1145\/3414080.3414089"},{"key":"3_CR30","doi-asserted-by":"publisher","unstructured":"Kirkeby, M.H., Gl\u00fcck, R.: Semi-inversion of conditional constructor term rewriting systems. In: Gabbrielli, M. (ed.) Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019, Porto, Portugal, October 8-10, 2019, Revised Selected Papers. Lecture Notes in Computer Science, vol. 12042, pp. 243\u2013259. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-45260-5_15","DOI":"10.1007\/978-3-030-45260-5_15"},{"key":"3_CR31","doi-asserted-by":"publisher","unstructured":"Kristensen, J.T., Kaarsgaard, R., Thomsen, M.K.: Jeopardy: An invertible functional programming language. Work-in-progress paper presented at 34th Symposium on Implementation and Application of Functional Languages abs\/2209.02422 (2022). https:\/\/doi.org\/10.48550\/arXiv.2209.02422","DOI":"10.48550\/arXiv.2209.02422"},{"key":"3_CR32","doi-asserted-by":"publisher","unstructured":"Landauer, R.: Irreversibility and heat generation in the computing process. IBM Journal of Research and Development 5(3), 183\u2013191 (1961). https:\/\/doi.org\/10.1147\/rd.53.0183","DOI":"10.1147\/rd.53.0183"},{"key":"3_CR33","doi-asserted-by":"publisher","unstructured":"Lindley, S., Wadler, P., Yallop, J.: The arrow calculus. J. Funct. Program. 20(1), 51\u201369 (2010). https:\/\/doi.org\/10.1017\/S095679680999027X","DOI":"10.1017\/S095679680999027X"},{"key":"3_CR34","doi-asserted-by":"publisher","unstructured":"Lindley, S., Wadler, P., Yallop, J.: Idioms are oblivious, arrows are meticulous, monads are promiscuous. Electron. Notes Theor. Comput. Sci. 229(5), 97\u2013117 (2011). https:\/\/doi.org\/10.1016\/j.entcs.2011.02.018","DOI":"10.1016\/j.entcs.2011.02.018"},{"key":"3_CR35","unstructured":"Lutz, C.: Janus: a time-reversible language (1986), Letter to R. Landauer. Available on: http:\/\/tetsuo.jp\/ref\/janus.pdf"},{"key":"3_CR36","doi-asserted-by":"publisher","unstructured":"Matsuda, K., Wang, M.: Applicative bidirectional programming with lenses. In: Fisher, K., Reppy, J.H. (eds.) ICFP. pp. 62\u201374. ACM (2015). https:\/\/doi.org\/10.1145\/2784731.2784750","DOI":"10.1145\/2784731.2784750"},{"key":"3_CR37","doi-asserted-by":"publisher","unstructured":"Matsuda, K., Wang, M.: Applicative bidirectional programming: Mixing lenses and semantic bidirectionalization. J. Funct. Program. 28, \u00a0e15 (2018). https:\/\/doi.org\/10.1017\/S0956796818000096","DOI":"10.1017\/S0956796818000096"},{"key":"3_CR38","doi-asserted-by":"publisher","unstructured":"Matsuda, K., Wang, M.: Hobit: Programming lenses without using lens combinators. In: Ahmed, A. (ed.) ESOP. Lecture Notes in Computer Science, vol. 10801, pp. 31\u201359. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_2","DOI":"10.1007\/978-3-319-89884-1_2"},{"key":"3_CR39","doi-asserted-by":"publisher","unstructured":"Matsuda, K., Wang, M.: Sparcl: A language for partially-invertible computation. Proc. ACM Program. Lang. 4(ICFP) (8 2020). https:\/\/doi.org\/10.1145\/3409000","DOI":"10.1145\/3409000"},{"key":"3_CR40","doi-asserted-by":"publisher","unstructured":"Matsuda, K., Wang, M.: Sparcl: A language for partially-invertible computation. J. Funct. Program. (in press). https:\/\/doi.org\/10.1017\/S0956796823000126","DOI":"10.1017\/S0956796823000126"},{"key":"3_CR41","doi-asserted-by":"publisher","unstructured":"Mogensen, T.\u00c6.: Semi-inversion of guarded equations. In: Gl\u00fcck, R., Lowry, M.R. (eds.) Generative Programming and Component Engineering, 4th International Conference, GPCE 2005, Tallinn, Estonia, September 29 - October 1, 2005, Proceedings. Lecture Notes in Computer Science, vol.\u00a03676, pp. 189\u2013204. Springer (2005). https:\/\/doi.org\/10.1007\/11561347_14","DOI":"10.1007\/11561347_14"},{"key":"3_CR42","doi-asserted-by":"publisher","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55\u201392 (1991). https:\/\/doi.org\/10.1016\/0890-5401(91)90052-4","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"3_CR43","doi-asserted-by":"publisher","unstructured":"Mu, S., Hu, Z., Takeichi, M.: An injective language for reversible computation. In: Kozen, D., Shankland, C. (eds.) Mathematics of Program Construction, 7th International Conference, MPC 2004, Stirling, Scotland, UK, July 12-14, 2004, Proceedings. Lecture Notes in Computer Science, vol.\u00a03125, pp. 289\u2013313. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-27764-4_16","DOI":"10.1007\/978-3-540-27764-4_16"},{"key":"3_CR44","doi-asserted-by":"publisher","unstructured":"Nishida, N., Sakai, M., Sakabe, T.: Partial inversion of constructor term rewriting systems. In: Giesl, J. (ed.) Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings. Lecture Notes in Computer Science, vol.\u00a03467, pp. 264\u2013278. Springer (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_20","DOI":"10.1007\/978-3-540-32033-3_20"},{"key":"3_CR45","unstructured":"Pierce, B.C.: Types and programming languages. MIT Press (2002)"},{"key":"3_CR46","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation 11(4), 363\u2013397 (1998). https:\/\/doi.org\/10.1023\/A:1010027404223","DOI":"10.1023\/A:1010027404223"},{"key":"3_CR47","doi-asserted-by":"publisher","unstructured":"Romanenko, A.: Inversion and metacomputation. In: Consel, C., Danvy, O. (eds.) Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM\u201991, Yale University, New Haven, Connecticut, USA, June 17-19, 1991. pp. 12\u201322. ACM (1991). https:\/\/doi.org\/10.1145\/115865.115868","DOI":"10.1145\/115865.115868"},{"key":"3_CR48","doi-asserted-by":"publisher","unstructured":"Sabry, A., Valiron, B., Vizzotto, J.K.: From symmetric pattern-matching to quantum control. In: Baier, C., Lago, U.D. (eds.) Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10803, pp. 348\u2013364. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_19","DOI":"10.1007\/978-3-319-89366-2_19"},{"key":"3_CR49","doi-asserted-by":"publisher","unstructured":"Srivastava, S., Gulwani, S., Chaudhuri, S., Foster, J.S.: Path-based inductive synthesis for program inversion. In: Hall, M.W., Padua, D.A. (eds.) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011. pp. 492\u2013503. ACM (2011). https:\/\/doi.org\/10.1145\/1993498.1993557","DOI":"10.1145\/1993498.1993557"},{"key":"3_CR50","doi-asserted-by":"crossref","unstructured":"Stinson, D., Paterson, M.: Cryptography: Theory and Practice. Textbooks in Mathematics, CRC Press (2018)","DOI":"10.1201\/9781315282497"},{"key":"3_CR51","doi-asserted-by":"publisher","unstructured":"Wadler, P.: A taste of linear logic. In: Borzyszkowski, A.M., Sokolowski, S. (eds.) Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS\u201993, Gdansk, Poland, August 30 - September 3, 1993, Proceedings. Lecture Notes in Computer Science, vol.\u00a0711, pp. 185\u2013210. Springer (1993). https:\/\/doi.org\/10.1007\/3-540-57182-5_12","DOI":"10.1007\/3-540-57182-5_12"},{"key":"3_CR52","doi-asserted-by":"publisher","unstructured":"Xia, L., Orchard, D., Wang, M.: Composing bidirectional programs monadically. In: Caires, L. (ed.) Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11423, pp. 147\u2013175. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17184-1_6","DOI":"10.1007\/978-3-030-17184-1_6"},{"key":"3_CR53","doi-asserted-by":"publisher","unstructured":"Yokoyama, T., Axelsen, H.B., Gl\u00fcck, R.: Principles of a reversible programming language. In: Ram\u00edrez, A., Bilardi, G., Gschwind, M. (eds.) Proceedings of the 5th Conference on Computing Frontiers, 2008, Ischia, Italy, May 5-7, 2008. pp. 43\u201354. ACM (2008). https:\/\/doi.org\/10.1145\/1366230.1366239","DOI":"10.1145\/1366230.1366239"},{"key":"3_CR54","doi-asserted-by":"publisher","unstructured":"Yokoyama, T., Axelsen, H.B., Gl\u00fcck, R.: Towards a reversible functional language. In: Vos, A.D., Wille, R. (eds.) RC. Lecture Notes in Computer Science, vol.\u00a07165, pp. 14\u201329. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-29517-1_2","DOI":"10.1007\/978-3-642-29517-1_2"}],"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-57267-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T16:03:06Z","timestamp":1712246586000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57267-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572661","9783031572678"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57267-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"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":"The accompanying artifact that contains the prototype implementation of <scp>Kalpis<\/scp> and the Agda formalization mentioned in this paper is available from .","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data Availability"}},{"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)"}}]}}