{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T04:27:37Z","timestamp":1752985657394,"version":"3.37.3"},"reference-count":65,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,1,29]],"date-time":"2024-01-29T00:00:00Z","timestamp":1706486400000},"content-version":"vor","delay-in-days":424,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000288","name":"Royal Society","doi-asserted-by":"crossref","award":["UF160079"],"award-info":[{"award-number":["UF160079"]}],"id":[{"id":"10.13039\/501100000288","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/T008911\/1"],"award-info":[{"award-number":["EP\/T008911\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000288","name":"Royal Society","doi-asserted-by":"crossref","award":["IESR3170104"],"award-info":[{"award-number":["IESR3170104"]}],"id":[{"id":"10.13039\/501100000288","id-type":"DOI","asserted-by":"crossref"}]},{"name":"JSPS KAKENHI","award":["15H02681","19K11892"],"award-info":[{"award-number":["15H02681","19K11892"]}]},{"name":"JSPS KAKENHI","award":["20H04161"],"award-info":[{"award-number":["20H04161"]}]},{"name":"JSPS Bilateral Program","award":["JPJSBP120199913"],"award-info":[{"award-number":["JPJSBP120199913"]}]},{"DOI":"10.13039\/100015333","name":"Kayamori Foundation of Informational Science Advancement","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100015333","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2022,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We propose a technique for synthesizing bidirectional programs from the corresponding unidirectional code plus input\/output examples. The core ideas are: (1) <jats:italic>constructing a sketch<\/jats:italic> using the given unidirectional program as a specification, and (2) <jats:italic>filling the sketch<\/jats:italic> in a modular fashion by exploiting the properties of bidirectional programs. These ideas are enabled by our choice of programming language, HOBiT, which is specifically designed to maintain the unidirectional program structure in bidirectional programming, and keep the parts that control bidirectional behavior modular. To evaluate our approach, we implemented it in a tool called <jats:sc>Synbit<\/jats:sc> and used it to generate bidirectional programs for intricate microbenchmarks, as well as for a few larger, more realistic problems. We also compared <jats:sc>Synbit<\/jats:sc> to a state-of-the-art unidirectional synthesis tool on the task of synthesizing backward computations. This is an extended version of the paper \u201cSynbit: Synthesizing Bidirectional Programs using Unidirectional Sketches\u201d, published at OOPSLA 2021. In addition to the OOPSLA\u201921 paper, this journal will contain additional formalization and detailed examples.\n<\/jats:p>","DOI":"10.1007\/s10703-023-00436-9","type":"journal-article","created":{"date-parts":[[2024,1,29]],"date-time":"2024-01-29T15:03:11Z","timestamp":1706540591000},"page":"198-247","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Synbit: synthesizing bidirectional programs using unidirectional sketches"],"prefix":"10.1007","volume":"61","author":[{"given":"Masaomi","family":"Yamaguchi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kazutaka","family":"Matsuda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9106-934X","authenticated-orcid":false,"given":"Cristina","family":"David","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meng","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,1,29]]},"reference":[{"issue":"4","key":"436_CR1","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1145\/319628.319634","volume":"6","author":"F Bancilhon","year":"1981","unstructured":"Bancilhon F, Spyratos N (1981) Update semantics of relational views. ACM Trans Database Syst 6(4):557\u2013575. https:\/\/doi.org\/10.1145\/319628.319634","journal-title":"ACM Trans Database Syst"},{"doi-asserted-by":"publisher","unstructured":"Hegner SJ (1990) Foundations of canonical update support for closed database views. In: ICDT, pp 422\u2013436. https:\/\/doi.org\/10.1007\/3-540-53507-1_93","key":"436_CR2","DOI":"10.1007\/3-540-53507-1_93"},{"doi-asserted-by":"publisher","unstructured":"Stevens P In: L\u00e4mmel R, Visser J, Saraiva J (eds) (2008) A landscape of bidirectional model transformations. Springer, Berlin, Heidelberg, pp 408\u2013424. https:\/\/doi.org\/10.1007\/978-3-540-88643-3_10","key":"436_CR3","DOI":"10.1007\/978-3-540-88643-3_10"},{"issue":"1145\/1232420","key":"436_CR4","first-page":"1232424","volume":"10","author":"JN Foster","year":"2007","unstructured":"Foster JN, Greenwald MB, Moore JT, Pierce BC, Schmitt A (2007) Combinators for bidirectional tree transformations: a linguistic approach to the view-update problem. ACM Trans Program Lang Syst 10(1145\/1232420):1232424","journal-title":"ACM Trans Program Lang Syst"},{"doi-asserted-by":"publisher","unstructured":"Matsuda K, Hu Z, Nakano K, Hamana M, Takeichi M (2007) Bidirectionalization transformation based on automatic derivation of view complement functions. In: Proceedings of the 12th ACM SIGPLAN international conference on functional programming, ICFP 2007, Freiburg, Germany, October 1\u20133, 2007, pp 47\u201358. https:\/\/doi.org\/10.1145\/1291151.1291162","key":"436_CR5","DOI":"10.1145\/1291151.1291162"},{"doi-asserted-by":"publisher","unstructured":"Bohannon A, Foster JN, Pierce BC, Pilkiewicz A, Schmitt A (2008) Boomerang: resourceful lenses for string data. In: Necula GC, Wadler P (eds) Proceedings of the 35th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pp 407\u2013419 . https:\/\/doi.org\/10.1145\/1328438.1328487","key":"436_CR6","DOI":"10.1145\/1328438.1328487"},{"doi-asserted-by":"publisher","unstructured":"Voigtl\u00e4nder J (2009) Bidirectionalization for free! (pearl). In: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages. POPL \u201909. Association for Computing Machinery, New York, NY, USA, pp 165\u2013176. https:\/\/doi.org\/10.1145\/1480881.1480904","key":"436_CR7","DOI":"10.1145\/1480881.1480904"},{"doi-asserted-by":"publisher","unstructured":"Pacheco H, Hu Z, Fischer S (2014) Monadic combinators for \"putback\" style bidirectional programming. In: Proceedings of the ACM SIGPLAN 2014 Workshop on partial evaluation and program manipulation, PEPM 2014, January 20\u201321, 2014, San Diego, California, USA, pp 39\u201350. https:\/\/doi.org\/10.1145\/2543728.2543737","key":"436_CR8","DOI":"10.1145\/2543728.2543737"},{"doi-asserted-by":"publisher","unstructured":"Matsuda K, Wang M (2018) Hobit: Programming lenses without using lens combinators. In: Ahmed A (ed) Programming languages and systems\u201427th European symposium on programming, ESOP 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14\u201320, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10801, pp 31\u201359. https:\/\/doi.org\/10.1007\/978-3-319-89884-1_2","key":"436_CR9","DOI":"10.1007\/978-3-319-89884-1_2"},{"doi-asserted-by":"publisher","unstructured":"Matsuda K, Wang M (2015) Applicative bidirectional programming with lenses. In: Proceedings of the 20th ACM SIGPLAN international conference on functional programming, ICFP 2015, Vancouver, BC, Canada, September 1\u20133, 2015, pp 62\u201374. https:\/\/doi.org\/10.1145\/2784731.2784750","key":"436_CR10","DOI":"10.1145\/2784731.2784750"},{"key":"436_CR11","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.scico.2014.07.008","volume":"111","author":"K Matsuda","year":"2015","unstructured":"Matsuda K, Wang M (2015) \u201cBidirectionalization for free\u2019\u2019 for monomorphic transformations. Sci Comput Program 111:79\u2013109. https:\/\/doi.org\/10.1016\/j.scico.2014.07.008","journal-title":"Sci Comput Program"},{"doi-asserted-by":"publisher","unstructured":"Chong N, Cook B, Kallas K, Khazem K, Monteiro FR, Schwartz-Narbonne D, Tasiran S, Tautschnig M, Tuttle MR (2020) Code-level model checking in the software development workflow. In: ICSE-SEIP 2020: 42nd international conference on software engineering, software engineering in practice, Seoul, South Korea, 27 June\u201319 July, 2020, pp 11\u201320. https:\/\/doi.org\/10.1145\/3377813.3381347","key":"436_CR12","DOI":"10.1145\/3377813.3381347"},{"doi-asserted-by":"publisher","unstructured":"Lubin J, Collins N, Omar C, Chugh R (2020) Program sketching with live bidirectional evaluation. In: Proceedings of the ACM on Programming Languages 4(ICFP), pp 109\u2013110929. https:\/\/doi.org\/10.1145\/3408991","key":"436_CR13","DOI":"10.1145\/3408991"},{"doi-asserted-by":"publisher","unstructured":"Gulwani S (2011) Automating string processing in spreadsheets using input-output examples. In: Ball T, Sagiv M (eds) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26\u201328, 2011, pp 317\u2013330. https:\/\/doi.org\/10.1145\/1926385.1926423","key":"436_CR14","DOI":"10.1145\/1926385.1926423"},{"doi-asserted-by":"publisher","unstructured":"Solar-Lezama A (2009) The sketching approach to program synthesis. In: Hu Z (ed) Programming languages and systems, 7th Asian symposium, APLAS 2009, Seoul, Korea, December 14\u201316, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5904, pp 4\u201313. https:\/\/doi.org\/10.1007\/978-3-642-10672-9_3","key":"436_CR15","DOI":"10.1007\/978-3-642-10672-9_3"},{"unstructured":"Lutz C (1986) Janus: a time-reversible language. Letter to R. Landauer. Available on: http:\/\/tetsuo.jp\/ref\/janus.pdf","key":"436_CR16"},{"doi-asserted-by":"publisher","unstructured":"Yokoyama T, Axelsen H.B, Gl\u00fcck R (2011) Towards a reversible functional language. In: RC, pp 14\u201329. https:\/\/doi.org\/10.1007\/978-3-642-29517-1_2","key":"436_CR17","DOI":"10.1007\/978-3-642-29517-1_2"},{"doi-asserted-by":"publisher","unstructured":"Ko H, Zan T, Hu Z (2016) BiGUL: a formally verified core language for putback-based bidirectional programming. In: Proceedings of the 2016 ACM SIGPLAN Workshop on partial evaluation and program manipulation, PEPM 2016, St. Petersburg, FL, USA, January 20\u201322, 2016, pp 61\u201372. https:\/\/doi.org\/10.1145\/2847538.2847544","key":"436_CR18","DOI":"10.1145\/2847538.2847544"},{"doi-asserted-by":"publisher","unstructured":"Hu Z, Ko H (2016) Principles and practice of bidirectional programming in BiGUL. In: Bidirectional transformations\u2014international summer school, Oxford, UK, July 25\u201329, 2016, Tutorial Lectures, pp 100\u2013150. https:\/\/doi.org\/10.1007\/978-3-319-79108-1_4","key":"436_CR19","DOI":"10.1007\/978-3-319-79108-1_4"},{"doi-asserted-by":"publisher","unstructured":"Jha S, Gulwani S, Seshia SA, Tiwari A (2010) Oracle-guided component-based program synthesis. In: Proceedings of the 32nd ACM\/IEEE international conference on software engineering\u2014Volume 1, ICSE 2010, Cape Town, South Africa, 1\u20138 May 2010, pp 215\u2013224. https:\/\/doi.org\/10.1145\/1806799.1806833","key":"436_CR20","DOI":"10.1145\/1806799.1806833"},{"doi-asserted-by":"crossref","unstructured":"Feng Y, Martins R, Wang Y, Dillig I, Reps TW (2017) Component-based synthesis for complex APIs. In: Proceedings of the 44th ACM SIGPLAN symposium on principles of programming languages, POPL 2017, Paris, France, January 18\u201320, 2017, pp 599\u2013612. http:\/\/dl.acm.org\/citation.cfm?id=3009851","key":"436_CR21","DOI":"10.1145\/3093333.3009851"},{"issue":"3","key":"436_CR22","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/382780.382785","volume":"48","author":"R Davies","year":"2001","unstructured":"Davies R, Pfenning F (2001) A modal analysis of staged computation. J ACM 48(3):555\u2013604. https:\/\/doi.org\/10.1145\/382780.382785","journal-title":"J ACM"},{"doi-asserted-by":"publisher","unstructured":"Osera P, Zdancewic S (2015) Type-and-example-directed program synthesis. In: Grove D, Blackburn SM (eds) Proceedings of the 36th ACM SIGPLAN conference on programming language design and implementation, Portland, OR, USA, June 15\u201317, 2015, pp 619\u2013630. https:\/\/doi.org\/10.1145\/2737924.2738007","key":"436_CR23","DOI":"10.1145\/2737924.2738007"},{"issue":"4\u20135","key":"436_CR24","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1017\/S0956796811000189","volume":"21","author":"S Fischer","year":"2011","unstructured":"Fischer S, Kiselyov O, Shan C (2011) Purely functional lazy nondeterministic programming. J Funct Program 21(4\u20135):413\u2013465. https:\/\/doi.org\/10.1017\/S0956796811000189","journal-title":"J Funct Program"},{"doi-asserted-by":"publisher","unstructured":"Albarghouthi A, Gulwani S, Kincaid Z (2013) Recursive program synthesis. In: Computer aided verification\u201425th international conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Proceedings, pp 934\u2013950. https:\/\/doi.org\/10.1007\/978-3-642-39799-8_67","key":"436_CR25","DOI":"10.1007\/978-3-642-39799-8_67"},{"doi-asserted-by":"publisher","unstructured":"Damas L, Milner R (1982) Principal type-schemes for functional programs. In: Conference record of the ninth annual ACM symposium on principles of programming languages, Albuquerque, New Mexico, USA, January 1982, pp 207\u2013212. https:\/\/doi.org\/10.1145\/582153.582176","key":"436_CR26","DOI":"10.1145\/582153.582176"},{"doi-asserted-by":"publisher","unstructured":"Matsuda K, Inaba K, Nakano K (2012) Polynomial-time inverse computation for accumulative functions with multiple data traversals. In: Proceedings of the ACM SIGPLAN 2012 workshop on partial evaluation and program manipulation, PEPM 2012, Philadelphia, Pennsylvania, USA, January 23\u201324, 2012, pp 5\u201314. https:\/\/doi.org\/10.1145\/2103746.2103752","key":"436_CR27","DOI":"10.1145\/2103746.2103752"},{"doi-asserted-by":"publisher","unstructured":"Nishida N, Vidal G (2011) Program inversion for tail recursive functions. In: Proceedings of the 22nd international conference on rewriting techniques and applications, RTA 2011, May 30\u2013June 1, 2011, Novi Sad, Serbia, pp 283\u2013298. https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2011.283","key":"436_CR28","DOI":"10.4230\/LIPIcs.RTA.2011.283"},{"doi-asserted-by":"publisher","unstructured":"de Jonge M, Visser E (2011) An algorithm for layout preservation in refactoring transformations. In: Software language engineering\u20144th international conference, SLE 2011, Braga, Portugal, July 3\u20134, 2011, Revised Selected Papers, pp 40\u201359. https:\/\/doi.org\/10.1007\/978-3-642-28830-2_3","key":"436_CR29","DOI":"10.1007\/978-3-642-28830-2_3"},{"doi-asserted-by":"publisher","unstructured":"Kort J, L\u00e4mmel R (2003) Parse-tree annotations meet re-engineering concerns. In: 3rd IEEE International workshop on source code analysis and manipulation (SCAM 2003), 26\u201327 September 2003, Amsterdam, The Netherlands, p 161. https:\/\/doi.org\/10.1109\/SCAM.2003.1238042","key":"436_CR30","DOI":"10.1109\/SCAM.2003.1238042"},{"doi-asserted-by":"publisher","unstructured":"Pombrio J, Krishnamurthi S (2014) Resugaring: lifting evaluation sequences through syntactic sugar. In: ACM SIGPLAN Conference on programming language design and implementation, PLDI \u201914, Edinburgh, United Kingdom\u2014June 09\u201311, 2014, pp 361\u2013371. https:\/\/doi.org\/10.1145\/2594291.2594319","key":"436_CR31","DOI":"10.1145\/2594291.2594319"},{"doi-asserted-by":"publisher","unstructured":"Miltner A, Fisher K, Pierce BC, Walker D, Zdancewic S (2018) Synthesizing bijective lenses. In: Proceedings of the ACM on Programming Languages 2(POPL), pp 1\u20131130. https:\/\/doi.org\/10.1145\/3158089","key":"436_CR32","DOI":"10.1145\/3158089"},{"doi-asserted-by":"publisher","unstructured":"Maina S, Miltner A, Fisher K, Pierce BC, Walker D, Zdancewic S (2018) Synthesizing quotient lenses. In: Proceedings of the ACM on Programming Languages 2(ICFP), pp 80\u201318029. https:\/\/doi.org\/10.1145\/3236775","key":"436_CR33","DOI":"10.1145\/3236775"},{"doi-asserted-by":"publisher","unstructured":"Miltner A, Maina S, Fisher K, Pierce BC, Walker D, Zdancewic S (2019) Synthesizing symmetric lenses. In: Proceedings of the ACM on Programming Languages 3(ICFP), pp 95\u201319528. https:\/\/doi.org\/10.1145\/3341699","key":"436_CR34","DOI":"10.1145\/3341699"},{"doi-asserted-by":"publisher","unstructured":"Hofmann M, Pierce BC, Wagner D (2011) Symmetric lenses. In: Proceedings of the 38th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2011, Austin, TX, USA, January 26\u201328, 2011, pp 371\u2013384. https:\/\/doi.org\/10.1145\/1926385.1926428","key":"436_CR35","DOI":"10.1145\/1926385.1926428"},{"doi-asserted-by":"publisher","unstructured":"Foster JN, Pilkiewicz A, Pierce BC (2008) Quotient lenses. In: Proceeding of the 13th ACM SIGPLAN international conference on functional programming, ICFP 2008, Victoria, BC, Canada, September 20\u201328, 2008, pp 383\u2013396. https:\/\/doi.org\/10.1145\/1411204.1411257","key":"436_CR36","DOI":"10.1145\/1411204.1411257"},{"doi-asserted-by":"publisher","unstructured":"Barbosa DMJ, Cretin J, Foster N, Greenberg M, Pierce BC (2010) Matching lenses: alignment and view update. In: Hudak P, Weirich S (eds) Proceeding of the 15th ACM SIGPLAN international conference on functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27\u201329, 2010, pp 193\u2013204. ACM,. https:\/\/doi.org\/10.1145\/1863543.1863572","key":"436_CR37","DOI":"10.1145\/1863543.1863572"},{"doi-asserted-by":"publisher","unstructured":"Voigtl\u00e4nder J (2012) Ideas for connecting inductive program synthesis and bidirectionalization. In: Proceedings of the ACM SIGPLAN 2012 workshop on partial evaluation and program manipulation, PEPM 2012, Philadelphia, Pennsylvania, USA, January 23\u201324, 2012, pp 39\u201342. https:\/\/doi.org\/10.1145\/2103746.2103757","key":"436_CR38","DOI":"10.1145\/2103746.2103757"},{"doi-asserted-by":"publisher","unstructured":"Srivastava S, Gulwani S, Chaudhuri S, Foster JS (2011) Path-based inductive synthesis for program inversion. In: Proceedings of the 32nd ACM SIGPLAN conference on programming language design and implementation, PLDI 2011, San Jose, CA, USA, June 4\u20138, 2011, pp 492\u2013503. https:\/\/doi.org\/10.1145\/1993498.1993557","key":"436_CR39","DOI":"10.1145\/1993498.1993557"},{"unstructured":"Korf RE (1981) Inversion of applicative programs. In: IJCAI, pp 1007\u20131009","key":"436_CR40"},{"doi-asserted-by":"publisher","unstructured":"Yokoyama T, Axelsen HB, Gl\u00fcck R (2008) Principles of a reversible programming language. In: Proceedings of the 5th conference on computing frontiers, 2008, Ischia, Italy, May 5\u20137, 2008, pp 43\u201354. https:\/\/doi.org\/10.1145\/1366230.1366239","key":"436_CR41","DOI":"10.1145\/1366230.1366239"},{"key":"436_CR42","volume-title":"The science of programming, chapter 21 inverting programs","author":"D Gries","year":"1981","unstructured":"Gries D (1981) The science of programming, chapter 21 inverting programs. Springer, Berlin"},{"issue":"5","key":"436_CR43","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/1071221.1071222","volume":"40","author":"R Gl\u00fcck","year":"2005","unstructured":"Gl\u00fcck R, Kawabe M (2005) Revisiting an automatic program inverter for lisp. SIGPLAN Not 40(5):8\u201317","journal-title":"SIGPLAN Not"},{"doi-asserted-by":"crossref","unstructured":"Matsuda K, Mu S-C, Hu Z, Takeichi M (2010) A grammar-based approach to invertible programs. In: ESOP, pp 448\u2013467","key":"436_CR44","DOI":"10.1007\/978-3-642-11957-6_24"},{"doi-asserted-by":"publisher","unstructured":"Nishida N, Sakai M, Sakabe T (2005) Partial inversion of constructor term rewriting systems. In: Term rewriting and applications, 16th international conference, RTA 2005, Nara, Japan, April 19\u201321, 2005, Proceedings, pp 264\u2013278. https:\/\/doi.org\/10.1007\/978-3-540-32033-3_20","key":"436_CR45","DOI":"10.1007\/978-3-540-32033-3_20"},{"issue":"1","key":"436_CR46","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1017\/S0956796800000058","volume":"1","author":"CK Gomard","year":"1991","unstructured":"Gomard CK, Jones ND (1991) A partial evaluator for the untyped lambda-calculus. J Funct Program 1(1):21\u201369. https:\/\/doi.org\/10.1017\/S0956796800000058","journal-title":"J Funct Program"},{"doi-asserted-by":"publisher","unstructured":"Almendros-Jim\u00e9nez JM, Vidal G (2006) Automatic partial inversion of inductively sequential functions. In: Implementation and application of functional languages, 18th international symposium, IFL 2006, Budapest, Hungary, September 4\u20136, 2006, Revised Selected Papers, pp 253\u2013270. https:\/\/doi.org\/10.1007\/978-3-540-74130-5_15","key":"436_CR47","DOI":"10.1007\/978-3-540-74130-5_15"},{"doi-asserted-by":"publisher","unstructured":"Matsuda K, Wang M (2020) Sparcl: a language for partially-invertible computation. In: Proceedings of the ACM on Programming Languages 4(ICFP), pp 118\u2013111831. https:\/\/doi.org\/10.1145\/3409000","key":"436_CR48","DOI":"10.1145\/3409000"},{"issue":"2","key":"436_CR49","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0304-3975(90)90147-A","volume":"73","author":"P Wadler","year":"1990","unstructured":"Wadler P (1990) Deforestation: transforming programs to eliminate trees. Theor Comput Sci 73(2):231\u2013248. https:\/\/doi.org\/10.1016\/0304-3975(90)90147-A","journal-title":"Theor Comput Sci"},{"doi-asserted-by":"publisher","unstructured":"Voigtl\u00e4nder J (2009) Bidirectionalization for free! (pearl). In: Proceedings of the 36th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2009, Savannah, GA, USA, January 21\u201323, 2009, pp 165\u2013176. https:\/\/doi.org\/10.1145\/1480881.1480904","key":"436_CR50","DOI":"10.1145\/1480881.1480904"},{"doi-asserted-by":"publisher","unstructured":"Wadler P (1989) Theorems for free! In: Proceedings of the fourth international conference on functional programming languages and computer architecture, FPCA 1989, London, UK, September 11\u201313, 1989, pp 347\u2013359. https:\/\/doi.org\/10.1145\/99370.99404","key":"436_CR51","DOI":"10.1145\/99370.99404"},{"unstructured":"Reynolds JC (1983) Types, abstraction and parametric polymorphism. In: Information processing 83, proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19\u201323, 1983, pp 513\u2013523","key":"436_CR52"},{"issue":"5","key":"436_CR53","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1017\/S0956796813000130","volume":"23","author":"J Voigtl\u00e4nder","year":"2013","unstructured":"Voigtl\u00e4nder J, Hu Z, Matsuda K, Wang M (2013) Enhancing semantic bidirectionalization via shape bidirectionalizer plug-ins. J Funct Program 23(5):515\u2013551. https:\/\/doi.org\/10.1017\/S0956796813000130","journal-title":"J Funct Program"},{"key":"436_CR54","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1017\/S0956796818000096","volume":"28","author":"K Matsuda","year":"2018","unstructured":"Matsuda K, Wang M (2018) Applicative bidirectional programming: Mixing lenses and semantic bidirectionalization. J Funct Program 28:15. https:\/\/doi.org\/10.1017\/S0956796818000096","journal-title":"J Funct Program"},{"doi-asserted-by":"publisher","unstructured":"Solar-Lezama A, Jones CG, Bod\u00edk R (2008) Sketching concurrent data structures. In: PLDI, pp 136\u2013148. https:\/\/doi.org\/10.1145\/1375581.1375599","key":"436_CR55","DOI":"10.1145\/1375581.1375599"},{"issue":"2","key":"436_CR56","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/3174802","volume":"40","author":"C David","year":"2018","unstructured":"David C, Kesseli P, Kroening D, Lewis M (2018) Program synthesis for program analysis. ACM Trans Program Lang Syst 40(2):5\u20131545. https:\/\/doi.org\/10.1145\/3174802","journal-title":"ACM Trans Program Lang Syst"},{"doi-asserted-by":"publisher","unstructured":"David C, Kroening D, Lewis M (2015) Unrestricted termination and non-termination arguments for bit-vector programs. In: Vitek J (ed) Programming languages and systems\u201424th European symposium on programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11\u201318, 2015. Proceedings. Lecture Notes in Computer Science, vol. 9032, pp 183\u2013204. https:\/\/doi.org\/10.1007\/978-3-662-46669-8_8","key":"436_CR57","DOI":"10.1007\/978-3-662-46669-8_8"},{"doi-asserted-by":"publisher","unstructured":"Abate A, Bessa I, Cattaruzza D, Cordeiro L.C, David C, Kesseli P, Kroening D, Polgreen E (2017) Automated formal synthesis of digital controllers for state-space physical plants. In: Majumdar R, Kuncak V (eds) Computer aided verification\u201429th international conference, CAV 2017, Heidelberg, Germany, July 24\u201328, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10426, pp 462\u2013482. https:\/\/doi.org\/10.1007\/978-3-319-63387-9_23","key":"436_CR58","DOI":"10.1007\/978-3-319-63387-9_23"},{"doi-asserted-by":"publisher","unstructured":"Kneuss E, Kuraj I, Kuncak V, Suter P (2013) Synthesis modulo recursive functions. In: Hosking AL, Eugster PT, Lopes CV (eds) Proceedings of the 2013 ACM SIGPLAN international conference on object oriented programming systems languages & applications, OOPSLA 2013, Part of SPLASH 2013, Indianapolis, IN, USA, October 26\u201331, 2013, pp 407\u2013426. https:\/\/doi.org\/10.1145\/2509136.2509555","key":"436_CR59","DOI":"10.1145\/2509136.2509555"},{"doi-asserted-by":"publisher","unstructured":"Abate A, David C, Kesseli P, Kroening D, Polgreen E (2018) Counterexample guided inductive synthesis modulo theories. In: Chockler H, Weissenbacher G (eds) Computer aided verification\u201430th international conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14\u201317, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, pp 270\u2013288. https:\/\/doi.org\/10.1007\/978-3-319-96145-3_15","key":"436_CR60","DOI":"10.1007\/978-3-319-96145-3_15"},{"unstructured":"Katayama S (2005) Systematic search for lambda expressions. In: van Eekelen MCJD","key":"#cr-split#-436_CR61.1"},{"unstructured":"(ed) Revised selected papers from the sixth symposium on trends in functional programming, TFP 2005, Tallinn, Estonia, 23-24 September 2005. Trends in Functional Programming, vol. 6, pp 111-126","key":"#cr-split#-436_CR61.2"},{"doi-asserted-by":"publisher","unstructured":"Feser JK, Chaudhuri S, Dillig I (2015) Synthesizing data structure transformations from input-output examples. In: Grove D, Blackburn SM (eds) Proceedings of the 36th ACM SIGPLAN conference on programming language design and implementation, Portland, OR, USA, June 15\u201317, 2015, pp 229\u2013239. https:\/\/doi.org\/10.1145\/2737924.2737977","key":"436_CR62","DOI":"10.1145\/2737924.2737977"},{"doi-asserted-by":"publisher","unstructured":"Smith C, Albarghouthi A (2019) Program synthesis with equivalence reduction. In: Enea C, Piskac R (eds) Verification, model checking, and abstract interpretation\u201420th international conference, VMCAI 2019, Cascais, Portugal, January 13\u201315, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11388, pp 24\u201347. https:\/\/doi.org\/10.1007\/978-3-030-11245-5_2","key":"436_CR63","DOI":"10.1007\/978-3-030-11245-5_2"},{"doi-asserted-by":"publisher","unstructured":"Koukoutos M, Kneuss E, Kuncak V (2016) An update on deductive synthesis and repair in the leon tool. In: Piskac R, Dimitrova R (eds) Proceedings fifth workshop on synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016. EPTCS, vol. 229, pp 100\u2013111. https:\/\/doi.org\/10.4204\/EPTCS.229.9","key":"436_CR64","DOI":"10.4204\/EPTCS.229.9"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00436-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00436-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00436-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,4]],"date-time":"2024-03-04T13:21:44Z","timestamp":1709558504000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00436-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12]]},"references-count":65,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["436"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00436-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2022,12]]},"assertion":[{"value":"1 April 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 June 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 January 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":"All the authors declare they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflicts of interest"}}]}}