{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:06:01Z","timestamp":1779836761496,"version":"3.53.1"},"reference-count":35,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2023,11,6]],"date-time":"2023-11-06T00:00:00Z","timestamp":1699228800000},"content-version":"unspecified","delay-in-days":309,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Bidirectional transformations (BXs) are a mechanism for maintaining consistency between multiple representations of related data. The lens framework, which usually constructs BXs from lens combinators, has become the mainstream approach to BX programming because of its modularity and correctness by construction. However, the involved bidirectional behaviors of lenses make the equational reasoning and optimization of them much harder than unidirectional programs. We propose a novel approach to deriving efficient lenses from clear specifications via program calculation, a correct-by-construction approach to reasoning about functional programs by algebraic laws. To support bidirectional program calculation, we propose\n                    <jats:italic>contract lenses<\/jats:italic>\n                    , which extend conventional lenses with a pair of predicates to enable safe and modular composition of partial lenses. We define several contract-lens combinators capturing common computation patterns including\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0956796823000059_inline1.png\"\/>\n                        <jats:tex-math>$\\textit{fold}, \\textit{filter},\\textit{map}$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    , and\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0956796823000059_inline2.png\"\/>\n                        <jats:tex-math>$\\textit{scan}$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    , and develop several bidirectional calculation laws to reason about and optimize contract lenses. We demonstrate the effectiveness of our new calculation framework based on contract lenses with nontrivial examples.\n                  <\/jats:p>","DOI":"10.1017\/s0956796823000059","type":"journal-article","created":{"date-parts":[[2023,11,6]],"date-time":"2023-11-06T05:02:50Z","timestamp":1699246970000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["Contract lenses: Reasoning about bidirectional programs via calculation"],"prefix":"10.1017","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3309-0439","authenticated-orcid":false,"given":"HANLIANG","family":"ZHANG","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-6589-3821","authenticated-orcid":false,"given":"WENHAO","family":"TANG","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7201-1954","authenticated-orcid":false,"given":"RUIFENG","family":"XIE","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7780-630X","authenticated-orcid":false,"given":"MENG","family":"WANG","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9034-205X","authenticated-orcid":false,"given":"ZHENJIANG","family":"HU","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2023,11,6]]},"reference":[{"key":"S0956796823000059_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926428"},{"key":"S0956796823000059_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88643-3_10"},{"key":"S0956796823000059_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.07.008"},{"key":"S0956796823000059_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-019-00736-x"},{"key":"S0956796823000059_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328487"},{"key":"S0956796823000059_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/1929501.1929520"},{"key":"S0956796823000059_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/232627.232637"},{"key":"S0956796823000059_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236070"},{"key":"S0956796823000059_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103715"},{"key":"S0956796823000059_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291162"},{"key":"S0956796823000059_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_6"},{"key":"S0956796823000059_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13321-3_19"},{"key":"S0956796823000059_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-79108-1_1"},{"key":"S0956796823000059_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480904"},{"key":"S0956796823000059_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863573"},{"key":"S0956796823000059_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863571"},{"key":"S0956796823000059_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416579"},{"key":"S0956796823000059_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2847538.2847544"},{"key":"S0956796823000059_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3409000"},{"key":"S0956796823000059_ref31","doi-asserted-by":"publisher","DOI":"10.14778\/3415478.3415503"},{"key":"S0956796823000059_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54804-8_3"},{"key":"S0956796823000059_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/1232420.1232424"},{"key":"S0956796823000059_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411257"},{"key":"S0956796823000059_ref5","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/32.2.122"},{"key":"S0956796823000059_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/1142351.1142399"},{"key":"S0956796823000059_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863572"},{"key":"S0956796823000059_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47797-7_5"},{"key":"S0956796823000059_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165214"},{"key":"S0956796823000059_ref19","unstructured":"Ko, H.-S. & Hu, Z. (2018) An axiomatic basis for bidirectional programming. In Proceedings of the 45th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, NY, USA: Association for Computing Machinery."},{"key":"S0956796823000059_ref12","doi-asserted-by":"crossref","unstructured":"Gibbons, J. (2011) Maximum segment sum, monadically (distilled tutorial). Electron. Proc. Theoret. Comput. Sci. 66, 181\u2013194.","DOI":"10.4204\/EPTCS.66.9"},{"key":"S0956796823000059_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/319628.319634"},{"key":"S0956796823000059_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-74884-4_5"},{"key":"S0956796823000059_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-87374-4_1"},{"key":"S0956796823000059_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784750"},{"key":"S0956796823000059_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_2"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796823000059","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:37:01Z","timestamp":1779835021000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796823000059\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"references-count":35,"alternative-id":["S0956796823000059"],"URL":"https:\/\/doi.org\/10.1017\/s0956796823000059","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e10"}}