HOBiT: Programming Lenses Without Using Lens
Combinators. In booktitleProgramming Languages and Systems
- 27th 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-20, 2018, Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume10801), editorpersonAmal
Ahmed (Ed.). publisherSpringer, pages31–59.

[Matsuda and WangMatsuda and Wang2020]
authorpersonKazutaka Matsuda and
personMeng Wang. year2020.
Sparcl: a language for partially-invertible
journalProc. ACM Program. Lang.
volume4, numberICFP (year2020),

[Miltner, Fisher, Pierce, Walker, and
ZdancewicMiltner et al2018]
authorpersonAnders Miltner, personKathleen
Fisher, personBenjamin C. Pierce, personDavid
Walker, and personSteve Zdancewic.
Synthesizing bijective lenses.
journalProc. ACM Program. Lang.
volume2, numberPOPL (year2018),

[Miltner, Maina, Fisher, Pierce, Walker, and
ZdancewicMiltner et al2019]
authorpersonAnders Miltner, personSolomon
Maina, personKathleen Fisher, personBenjamin C.
Pierce, personDavid Walker, and personSteve
Zdancewic. year2019.
Synthesizing symmetric lenses.
journalProc. ACM Program. Lang.
volume3, numberICFP (year2019),

[Nishida, Sakai, and SakabeNishida
et al2005]
authorpersonNaoki Nishida, personMasahiko
Sakai, and personToshiki Sakabe.
Partial Inversion of Constructor Term Rewriting
Systems. In booktitleTerm Rewriting and Applications, 16th
International Conference, RTA 2005, Nara, Japan, April 19-21, 2005,
Proceedings (seriesLecture Notes in Computer Science,
Vol. volume3467),
editorpersonJürgen Giesl (Ed.).
publisherSpringer, pages264–278.

[Nishida and VidalNishida and Vidal2011]
authorpersonNaoki Nishida and
personGermán Vidal. year2011.
Program Inversion for Tail Recursive Functions. In
booktitleProceedings of the 22nd International Conference on
Rewriting Techniques and Applications, RTA 2011, May 30 - June 1, 2011,
Novi Sad, Serbia (seriesLIPIcs,
Vol. volume10), editorpersonManfred
Schmidt-Schauß (Ed.). publisherSchloss Dagstuhl -
Leibniz-Zentrum für Informatik, pages283–298.

[Osera and ZdancewicOsera and
authorpersonPeter-Michael Osera and
personSteve Zdancewic. year2015.
Type-and-example-directed program synthesis. In
booktitleProceedings of the 36th ACM SIGPLAN Conference
on Programming Language Design and Implementation, Portland, OR, USA, June
15-17, 2015, editorpersonDavid Grove and
personStephen M. Blackburn (Eds.). publisherACM,

[Pacheco, Hu, and FischerPacheco
et al2014]
authorpersonHugo Pacheco, personZhenjiang
Hu, and personSebastian Fischer.
Monadic combinators for "Putback" style
bidirectional programming. In booktitleProceedings of the
ACM SIGPLAN 2014 workshop on Partial evaluation and program manipulation,
PEPM 2014, January 20-21, 2014, San Diego, California, USA,
editorpersonWei-Ngan Chin and
personJurriaan Hage (Eds.). publisherACM,

[Pombrio and KrishnamurthiPombrio and
authorpersonJustin Pombrio and
personShriram Krishnamurthi. year2014.
Resugaring: lifting evaluation sequences through
syntactic sugar. In booktitleACM SIGPLAN Conference on
Programming Language Design and Implementation, PLDI '14, Edinburgh, United
Kingdom - June 09 - 11, 2014, editorpersonMichael
F. P. O'Boyle and personKeshav Pingali (Eds.).
publisherACM, pages361–371.

authorpersonJohn C. Reynolds.
Types, Abstraction and Parametric Polymorphism. In
booktitleInformation Processing 83, Proceedings of the
IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983,
editorpersonR. E. A. Mason (Ed.).
publisherNorth-Holland/IFIP, pages513–523.

[Smith and AlbarghouthiSmith and
authorpersonCalvin Smith and personAws
Albarghouthi. year2019.
Program Synthesis with Equivalence Reduction. In
booktitleVerification, Model Checking, and Abstract
Interpretation - 20th International Conference, VMCAI 2019, Cascais,
Portugal, January 13-15, 2019, Proceedings (seriesLecture
Notes in Computer Science, Vol. volume11388),
editorpersonConstantin Enea and
personRuzica Piskac (Eds.). publisherSpringer,

authorpersonArmando Solar-Lezama.
The Sketching Approach to Program Synthesis. In
booktitleProgramming Languages and Systems, 7th Asian
Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume5904), editorpersonZhenjiang
Hu (Ed.). publisherSpringer, pages4–13.

[Solar-Lezama, Jones, and
BodíkSolar-Lezama et al2008]
authorpersonArmando Solar-Lezama,
personChristopher Grant Jones, and personRastislav
Bodík. year2008.
Sketching concurrent data structures. In
booktitlePLDI. pages136–148.

[Srivastava, Gulwani, Chaudhuri, and
FosterSrivastava et al2011]
authorpersonSaurabh Srivastava, personSumit
Gulwani, personSwarat Chaudhuri, and
personJeffrey S. Foster. year2011.
Path-based inductive synthesis for program
inversion. In booktitleProceedings of the 32nd ACM
SIGPLAN Conference on Programming Language Design and Implementation,
PLDI 2011, San Jose, CA, USA, June 4-8, 2011,
editorpersonMary W. Hall and
personDavid A. Padua (Eds.). publisherACM,

authorpersonPerdita Stevens.
booktitleA Landscape of Bidirectional Model
publisherSpringer Berlin Heidelberg,
addressBerlin, Heidelberg, pages408–424.

authorpersonJanis Voigtländer.
Bidirectionalization for Free! (Pearl). In
booktitleProceedings of the 36th Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (Savannah, GA, USA)
(seriesPOPL '09). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

authorpersonJanis Voigtländer.
Bidirectionalization for free! (Pearl). In
booktitleProceedings of the 36th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA,
USA, January 21-23, 2009, editorpersonZhong Shao
and personBenjamin C. Pierce (Eds.).
publisherACM, pages165–176.

authorpersonJanis Voigtländer.
Ideas for connecting inductive program synthesis
and bidirectionalization, See DBLP:conf/pepm/2012,

[Voigtländer, Hu, Matsuda, and
WangVoigtländer et al2013]
authorpersonJanis Voigtländer,
personZhenjiang Hu, personKazutaka Matsuda, and
personMeng Wang. year2013.
Enhancing semantic bidirectionalization via shape
bidirectionalizer plug-ins.
journalJ. Funct. Program. volume23,
number5 (year2013), pages515–551.

authorpersonPhilip Wadler.
Theorems for Free!. In
booktitleProceedings of the fourth international conference
on Functional programming languages and computer architecture, FPCA 1989,
London, UK, September 11-13, 1989,
editorpersonJoseph E. Stoy (Ed.).
publisherACM, pages347–359.

authorpersonPhilip Wadler.
Deforestation: Transforming Programs to Eliminate
journalTheor. Comput. Sci. volume73,
number2 (year1990), pages231–248.

[Yamaguchi, Matsuda, David, and WangYamaguchi
et al2021]
authorpersonMasaomi Yamaguchi,
personKazutaka Matsuda, personCristina David, and
personMeng Wang. year2021.
Synbit: Synthesizing Bidirectional Programs
using Unidirectional Sketches.
journalCoRR  volumeabs/2108.13783

[Yokoyama, Axelsen, and GlückYokoyama
et al2008]
authorpersonTetsuo Yokoyama,
personHolger Bock Axelsen, and personRobert
Glück. year2008.
Principles of a reversible programming language.
In booktitleProceedings of the 5th Conference on Computing
Frontiers, 2008, Ischia, Italy, May 5-7, 2008,
editorpersonAlex Ramírez,
personGianfranco Bilardi, and personMichael
Gschwind (Eds.). publisherACM, pages43–54.

[Yokoyama, Axelsen, and GlückYokoyama
et al2011]
authorpersonTetsuo Yokoyama,
personHolger Bock Axelsen, and personRobert
Glück. year2011.
Towards a Reversible Functional Language. In
booktitleRC (seriesLecture Notes in
Computer Science, Vol. volume7165),
editorpersonAlexis De Vos and
personRobert Wille (Eds.). publisherSpringer,

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Abate, Bessa, Cattaruzza, Cordeiro, David,
Kesseli, Kroening, and PolgreenAbate et al2017]
authorpersonAlessandro Abate, personIury
Bessa, personDario Cattaruzza, personLucas C.
Cordeiro, personCristina David, personPascal
Kesseli, personDaniel Kroening, and personElizabeth
Polgreen. year2017.
Automated Formal Synthesis of Digital Controllers
for State-Space Physical Plants. In booktitleComputer Aided
Verification - 29th International Conference, CAV 2017, Heidelberg,
Germany, July 24-28, 2017, Proceedings, Part I
(seriesLecture Notes in Computer Science,
Vol. volume10426), editorpersonRupak
Majumdar and personViktor Kuncak (Eds.).
publisherSpringer, pages462–482.

[Abate, David, Kesseli, Kroening, and
PolgreenAbate et al2018]
authorpersonAlessandro Abate, personCristina
David, personPascal Kesseli, personDaniel Kroening,
and personElizabeth Polgreen. year2018.
Counterexample Guided Inductive Synthesis Modulo
Theories. In booktitleComputer Aided Verification - 30th
International Conference, CAV 2018, Held as Part of the Federated Logic
Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I
(seriesLecture Notes in Computer Science,
Vol. volume10981), editorpersonHana
Chockler and personGeorg Weissenbacher (Eds.).
publisherSpringer, pages270–288.

[Albarghouthi, Gulwani, and
KincaidAlbarghouthi et al2013]
authorpersonAws Albarghouthi, personSumit
Gulwani, and personZachary Kincaid.
Recursive Program Synthesis. In
booktitleComputer Aided Verification - 25th International
Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013.
Proceedings (seriesLecture Notes in Computer Science,
Vol. volume8044), editorpersonNatasha
Sharygina and personHelmut Veith (Eds.).
publisherSpringer, pages934–950.

[Almendros-Jiménez and
VidalAlmendros-Jiménez and Vidal2006]
authorpersonJesús Manuel
Almendros-Jiménez and personGermán Vidal.
Automatic Partial Inversion of Inductively
Sequential Functions. In booktitleImplementation and
Application of Functional Languages, 18th International Symp osium, IFL
2006, Budapest, Hungary, September 4-6, 2006, Revised Selected Papers
(seriesLecture Notes in Computer Science,
Vol. volume4449),
editorpersonZoltán Horváth,
personViktória Zsók, and personAndrew
Butterfield (Eds.). publisherSpringer,

[Bancilhon and SpyratosBancilhon and
authorpersonFrançois Bancilhon and
personNicolas Spyratos. year1981.
Update Semantics of Relational Views.
journalACM Trans. Database Syst.
volume6, number4 (year1981),

[Bohannon, Foster, Pierce, Pilkiewicz, and
SchmittBohannon et al2008]
authorpersonAaron Bohannon, personJ. Nathan
Foster, personBenjamin C. Pierce, personAlexandre
Pilkiewicz, and personAlan Schmitt.
Boomerang: resourceful lenses for string data. In
booktitleProceedings of the 35th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2008, San Francisco,
California, USA, January 7-12, 2008,
editorpersonGeorge C. Necula and
personPhilip Wadler (Eds.). publisherACM,

[Chong, Cook, Kallas, Khazem, Monteiro,
Schwartz-Narbonne, Tasiran, Tautschnig, and TuttleChong
et al2020]
authorpersonNathan Chong, personByron Cook,
personKonstantinos Kallas, personKareem Khazem,
personFelipe R. Monteiro, personDaniel
Schwartz-Narbonne, personSerdar Tasiran,
personMichael Tautschnig, and personMark R.
Tuttle. year2020.
Code-level model checking in the software
development workflow. In booktitleICSE-SEIP 2020: 42nd
International Conference on Software Engineering, Software Engineering in
Practice, Seoul, South Korea, 27 June - 19 July, 2020,
editorpersonGregg Rothermel and
personDoo-Hwan Bae (Eds.). publisherACM,

[Damas and MilnerDamas and Milner1982]
authorpersonLuís Damas and
personRobin Milner. year1982.
Principal Type-Schemes for Functional Programs. In
booktitleConference Record of the Ninth Annual ACM
Symposium on Principles of Programming Languages, Albuquerque, New Mexico,
USA, January 1982, editorpersonRichard A. DeMillo
(Ed.). publisherACM Press, pages207–212.

[David, Kesseli, Kroening, and LewisDavid
et al2018]
authorpersonCristina David, personPascal
Kesseli, personDaniel Kroening, and personMatt
Lewis. year2018.
Program Synthesis for Program Analysis.
journalACM Trans. Program. Lang. Syst.
volume40, number2 (year2018),

[David, Kroening, and LewisDavid
et al2015]
authorpersonCristina David, personDaniel
Kroening, and personMatt Lewis.
Unrestricted Termination and Non-termination
Arguments for Bit-Vector Programs. In booktitleProgramming
Languages and Systems - 24th 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-18, 2015. Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume9032), editorpersonJan Vitek
(Ed.). publisherSpringer, pages183–204.

[Davies and PfenningDavies and
authorpersonRowan Davies and personFrank
Pfenning. year2001.
A modal analysis of staged computation.
journalJ. ACM volume48,
number3 (year2001), pages555–604.

[de Jonge and Visserde Jonge and
authorpersonMaartje de Jonge and
personEelco Visser. year2011.
An Algorithm for Layout Preservation in Refactoring
Transformations. In booktitleSoftware Language Engineering
- 4th International Conference, SLE 2011, Braga, Portugal, July 3-4, 2011,
Revised Selected Papers (seriesLecture Notes in Computer
Science, Vol. volume6940),
editorpersonAnthony M. Sloane and
personUwe Aßmann (Eds.). publisherSpringer,

[Feng, Martins, Wang, Dillig, and RepsFeng
et al2017]
authorpersonYu Feng, personRuben Martins,
personYuepeng Wang, personIsil Dillig, and
personThomas W. Reps. year2017.
Component-based synthesis for complex APIs. In
booktitleProceedings of the 44th ACM SIGPLAN Symposium
on Principles of Programming Languages, POPL 2017, Paris, France, January
18-20, 2017, editorpersonGiuseppe Castagna and
personAndrew D. Gordon (Eds.). publisherACM,

[Feser, Chaudhuri, and DilligFeser
et al2015]
authorpersonJohn K. Feser, personSwarat
Chaudhuri, and personIsil Dillig.
Synthesizing data structure transformations from
input-output examples. In booktitleProceedings of the 36th
ACM SIGPLAN Conference on Programming Language Design and Implementation,
Portland, OR, USA, June 15-17, 2015,
editorpersonDavid Grove and
personStephen M. Blackburn (Eds.). publisherACM,

[Fischer, Kiselyov, and ShanFischer
et al2011]
authorpersonSebastian Fischer, personOleg
Kiselyov, and personChung-chieh Shan.
Purely functional lazy nondeterministic
journalJ. Funct. Program. volume21,
number4-5 (year2011), pages413–465.

[Foster, Greenwald, Moore, Pierce, and
SchmittFoster et al2007]
authorpersonJ. Nathan Foster,
personMichael B. Greenwald, personJonathan T. Moore,
personBenjamin C. Pierce, and personAlan Schmitt.
Combinators for bidirectional tree transformations:
A linguistic approach to the view-update problem.
journalACM Trans. Program. Lang. Syst.
volume29, number3 (year2007).

[Foster, Pilkiewicz, and PierceFoster
et al2008]
authorpersonJ. Nathan Foster,
personAlexandre Pilkiewicz, and personBenjamin C.
Pierce. year2008.
Quotient lenses. In
booktitleProceeding of the 13th ACM SIGPLAN
international conference on Functional programming, ICFP 2008, Victoria,
BC, Canada, September 20-28, 2008, editorpersonJames
Hook and personPeter Thiemann (Eds.).
publisherACM, pages383–396.

[Glück and KawabeGlück and
authorpersonRobert Glück and
personMasahiko Kawabe. year2005.
Revisiting an automatic program inverter for Lisp.
journalSIGPLAN Notices volume40,
number5 (year2005), pages8–17.

[Gomard and JonesGomard and Jones1991]
authorpersonCarsten K. Gomard and
personNeil D. Jones. year1991.
A Partial Evaluator for the Untyped
journalJ. Funct. Program. volume1,
number1 (year1991), pages21–69.

authorpersonDavid Gries.
booktitleThe Science of Programming.
publisherSpringer, Heidelberg, Chapter 21 Inverting

authorpersonSumit Gulwani.
Automating string processing in spreadsheets using
input-output examples. In booktitleProceedings of the 38th
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL 2011, Austin, TX, USA, January 26-28, 2011,
editorpersonThomas Ball and personMooly
Sagiv (Eds.). publisherACM, pages317–330.

authorpersonStephen J. Hegner.
Foundations of Canonical Update Support for Closed
Database Views. In booktitleICDT
(seriesLecture Notes in Computer Science,
Vol. volume470), editorpersonSerge
Abiteboul and personParis C. Kanellakis (Eds.).
publisherSpringer, pages422–436.

[Hofmann, Pierce, and WagnerHofmann
et al2011]
authorpersonMartin Hofmann,
personBenjamin C. Pierce, and personDaniel Wagner.
Symmetric lenses. In
booktitleProceedings of the 38th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2011, Austin, TX,
USA, January 26-28, 2011, editorpersonThomas Ball
and personMooly Sagiv (Eds.). publisherACM,

[Hu and KoHu and Ko2016]
authorpersonZhenjiang Hu and
personHsiang-Shang Ko. year2016.
Principles and Practice of Bidirectional
Programming in BiGUL. In booktitleBidirectional
Transformations - International Summer School, Oxford, UK, July 25-29, 2016,
Tutorial Lectures (seriesLecture Notes in Computer
Science, Vol. volume9715),
editorpersonJeremy Gibbons and
personPerdita Stevens (Eds.). publisherSpringer,

[Jha, Gulwani, Seshia, and TiwariJha
et al2010]
authorpersonSusmit Jha, personSumit
Gulwani, personSanjit A. Seshia, and personAshish
Tiwari. year2010.
Oracle-guided component-based program synthesis.
In booktitleProceedings of the 32nd ACM/IEEE International
Conference on Software Engineering - Volume 1, ICSE 2010, Cape Town, South
Africa, 1-8 May 2010, editorpersonJeff Kramer,
personJudith Bishop, personPremkumar T. Devanbu,
and personSebastián Uchitel (Eds.).
publisherACM, pages215–224.

authorpersonSusumu Katayama.
Systematic search for lambda expressions. In
booktitleRevised Selected Papers from the Sixth Symposium on
Trends in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24
September 2005 (seriesTrends in Functional Programming,
Vol. volume6), editorpersonMarko C. J. D.
van Eekelen (Ed.). publisherIntellect,

[Kiselyov and ThompsonKiselyov and
editorpersonOleg Kiselyov and
personSimon J. Thompson (Eds.). year2012.
booktitleProceedings of the ACM SIGPLAN 2012
Workshop on Partial Evaluation and Program Manipulation, PEPM 2012,
Philadelphia, Pennsylvania, USA, January 23-24, 2012.

[Kneuss, Kuraj, Kuncak, and SuterKneuss
et al2013]
authorpersonEtienne Kneuss, personIvan
Kuraj, personViktor Kuncak, and personPhilippe
Suter. year2013.
Synthesis modulo recursive functions. In
booktitleProceedings 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-31, 2013, editorpersonAntony L.
Hosking, personPatrick Th. Eugster, and
personCristina V. Lopes (Eds.). publisherACM,

[Ko, Zan, and HuKo et al2016]
authorpersonHsiang-Shang Ko, personTao
Zan, and personZhenjiang Hu. year2016.
BiGUL: a formally verified core language for
putback-based bidirectional programming. In
booktitleProceedings of the 2016 ACM SIGPLAN Workshop on
Partial Evaluation and Program Manipulation, PEPM 2016, St. Petersburg, FL,
USA, January 20 - 22, 2016, editorpersonMartin
Erwig and personTiark Rompf (Eds.).
publisherACM, pages61–72.

authorpersonRichard E. Korf.
Inversion of Applicative Programs. In
editorpersonPatrick J. Hayes (Ed.).
publisherWilliam Kaufmann, pages1007–1009.

[Kort and LämmelKort and
authorpersonJan Kort and personRalf
Lämmel. year2003.
Parse-Tree Annotations Meet Re-Engineering
Concerns. In booktitle3rd IEEE International Workshop on
Source Code Analysis and Manipulation (SCAM 2003), 26-27 September 2003,
Amsterdam, The Netherlands. publisherIEEE Computer Society,

[Koukoutos, Kneuss, and KuncakKoukoutos
et al2016]
authorpersonManos Koukoutos, personEtienne
Kneuss, and personViktor Kuncak.
An Update on Deductive Synthesis and Repair in the
Leon Tool. In booktitleProceedings Fifth Workshop on
Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016
(seriesEPTCS, Vol. volume229),
editorpersonRuzica Piskac and
personRayna Dimitrova (Eds.). pages100–111.

[Lubin, Collins, Omar, and ChughLubin
et al2020]
authorpersonJustin Lubin, personNick
Collins, personCyrus Omar, and personRavi Chugh.
Program sketching with live bidirectional
journalProc. ACM Program. Lang.
volume4, numberICFP (year2020),

authorpersonChristopher Lutz.
titleJanus: a time-reversible language.
Letter to R. Landauer. Available on:

[Maina, Miltner, Fisher, Pierce, Walker, and
ZdancewicMaina et al2018]
authorpersonSolomon Maina, personAnders
Miltner, personKathleen Fisher, personBenjamin C.
Pierce, personDavid Walker, and personSteve
Zdancewic. year2018.
Synthesizing quotient lenses.
journalProc. ACM Program. Lang.
volume2, numberICFP (year2018),

[Matsuda, Hu, Nakano, Hamana, and
TakeichiMatsuda et al2007]
authorpersonKazutaka Matsuda,
personZhenjiang Hu, personKeisuke Nakano,
personMakoto Hamana, and personMasato Takeichi.
Bidirectionalization transformation based on
automatic derivation of view complement functions. In
booktitleProceedings of the 12th ACM SIGPLAN
International Conference on Functional Programming, ICFP 2007, Freiburg,
Germany, October 1-3, 2007, editorpersonRalf Hinze
and personNorman Ramsey (Eds.). publisherACM,

[Matsuda, Inaba, and NakanoMatsuda
et al2012]
authorpersonKazutaka Matsuda, personKazuhiro
Inaba, and personKeisuke Nakano.
Polynomial-time inverse computation for
accumulative functions with multiple data traversals, See
DBLP:conf/pepm/2012, pages5–14.

[Matsuda, Mu, Hu, and TakeichiMatsuda
et al2010]
authorpersonKazutaka Matsuda,
personShin-Cheng Mu, personZhenjiang Hu, and
personMasato Takeichi. year2010.
A Grammar-Based Approach to Invertible Programs.
In booktitleESOP (seriesLecture Notes in
Computer Science, Vol. volume6012),
editorpersonAndrew D. Gordon (Ed.).
publisherSpringer, pages448–467.

[Matsuda and WangMatsuda and Wang2015a]
authorpersonKazutaka Matsuda and
personMeng Wang. year2015a.
Applicative bidirectional programming with lenses.
In booktitleProceedings of the 20th ACM SIGPLAN
International Conference on Functional Programming, ICFP 2015, Vancouver,
BC, Canada, September 1-3, 2015,
editorpersonKathleen Fisher and
personJohn H. Reppy (Eds.). publisherACM,

[Matsuda and WangMatsuda and Wang2015b]
authorpersonKazutaka Matsuda and
personMeng Wang. year2015b.
"Bidirectionalization for free" for monomorphic
journalSci. Comput. Program.
volume111 (year2015), pages79–109.

[Matsuda and WangMatsuda and Wang2018a]
authorpersonKazutaka Matsuda and
personMeng Wang. year2018a.
Applicative bidirectional programming: Mixing
lenses and semantic bidirectionalization.
journalJ. Funct. Program.  volume28
(year2018), pagese15.

[Matsuda and WangMatsuda and Wang2018b]
Matsuda   Wang:2018:HOBiT
authorpersonKazutaka Matsuda and
personMeng Wang. year2018b.
HOBiT: Programming Lenses Without Using Lens
Combinators. In booktitleProgramming Languages and Systems
- 27th 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-20, 2018, Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume10801), editorpersonAmal
Ahmed (Ed.). publisherSpringer, pages31–59.

[Matsuda and WangMatsuda and Wang2020]
authorpersonKazutaka Matsuda and
personMeng Wang. year2020.
Sparcl: a language for partially-invertible
journalProc. ACM Program. Lang.
volume4, numberICFP (year2020),

[Miltner, Fisher, Pierce, Walker, and
ZdancewicMiltner et al2018]
authorpersonAnders Miltner, personKathleen
Fisher, personBenjamin C. Pierce, personDavid
Walker, and personSteve Zdancewic.
Synthesizing bijective lenses.
journalProc. ACM Program. Lang.
volume2, numberPOPL (year2018),

[Miltner, Maina, Fisher, Pierce, Walker, and
ZdancewicMiltner et al2019]
authorpersonAnders Miltner, personSolomon
Maina, personKathleen Fisher, personBenjamin C.
Pierce, personDavid Walker, and personSteve
Zdancewic. year2019.
Synthesizing symmetric lenses.
journalProc. ACM Program. Lang.
volume3, numberICFP (year2019),

[Nishida, Sakai, and SakabeNishida
et al2005]
authorpersonNaoki Nishida, personMasahiko
Sakai, and personToshiki Sakabe.
Partial Inversion of Constructor Term Rewriting
Systems. In booktitleTerm Rewriting and Applications, 16th
International Conference, RTA 2005, Nara, Japan, April 19-21, 2005,
Proceedings (seriesLecture Notes in Computer Science,
Vol. volume3467),
editorpersonJürgen Giesl (Ed.).
publisherSpringer, pages264–278.

[Nishida and VidalNishida and Vidal2011]
authorpersonNaoki Nishida and
personGermán Vidal. year2011.
Program Inversion for Tail Recursive Functions. In
booktitleProceedings of the 22nd International Conference on
Rewriting Techniques and Applications, RTA 2011, May 30 - June 1, 2011,
Novi Sad, Serbia (seriesLIPIcs,
Vol. volume10), editorpersonManfred
Schmidt-Schauß (Ed.). publisherSchloss Dagstuhl -
Leibniz-Zentrum für Informatik, pages283–298.

[Osera and ZdancewicOsera and
authorpersonPeter-Michael Osera and
personSteve Zdancewic. year2015.
Type-and-example-directed program synthesis. In
booktitleProceedings of the 36th ACM SIGPLAN Conference
on Programming Language Design and Implementation, Portland, OR, USA, June
15-17, 2015, editorpersonDavid Grove and
personStephen M. Blackburn (Eds.). publisherACM,

[Pacheco, Hu, and FischerPacheco
et al2014]
authorpersonHugo Pacheco, personZhenjiang
Hu, and personSebastian Fischer.
Monadic combinators for "Putback" style
bidirectional programming. In booktitleProceedings of the
ACM SIGPLAN 2014 workshop on Partial evaluation and program manipulation,
PEPM 2014, January 20-21, 2014, San Diego, California, USA,
editorpersonWei-Ngan Chin and
personJurriaan Hage (Eds.). publisherACM,

[Pombrio and KrishnamurthiPombrio and
authorpersonJustin Pombrio and
personShriram Krishnamurthi. year2014.
Resugaring: lifting evaluation sequences through
syntactic sugar. In booktitleACM SIGPLAN Conference on
Programming Language Design and Implementation, PLDI '14, Edinburgh, United
Kingdom - June 09 - 11, 2014, editorpersonMichael
F. P. O'Boyle and personKeshav Pingali (Eds.).
publisherACM, pages361–371.

authorpersonJohn C. Reynolds.
Types, Abstraction and Parametric Polymorphism. In
booktitleInformation Processing 83, Proceedings of the
IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983,
editorpersonR. E. A. Mason (Ed.).
publisherNorth-Holland/IFIP, pages513–523.

[Smith and AlbarghouthiSmith and
authorpersonCalvin Smith and personAws
Albarghouthi. year2019.
Program Synthesis with Equivalence Reduction. In
booktitleVerification, Model Checking, and Abstract
Interpretation - 20th International Conference, VMCAI 2019, Cascais,
Portugal, January 13-15, 2019, Proceedings (seriesLecture
Notes in Computer Science, Vol. volume11388),
editorpersonConstantin Enea and
personRuzica Piskac (Eds.). publisherSpringer,

authorpersonArmando Solar-Lezama.
The Sketching Approach to Program Synthesis. In
booktitleProgramming Languages and Systems, 7th Asian
Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume5904), editorpersonZhenjiang
Hu (Ed.). publisherSpringer, pages4–13.

[Solar-Lezama, Jones, and
BodíkSolar-Lezama et al2008]
authorpersonArmando Solar-Lezama,
personChristopher Grant Jones, and personRastislav
Bodík. year2008.
Sketching concurrent data structures. In
booktitlePLDI. pages136–148.

[Srivastava, Gulwani, Chaudhuri, and
FosterSrivastava et al2011]
authorpersonSaurabh Srivastava, personSumit
Gulwani, personSwarat Chaudhuri, and
personJeffrey S. Foster. year2011.
Path-based inductive synthesis for program
inversion. In booktitleProceedings of the 32nd ACM
SIGPLAN Conference on Programming Language Design and Implementation,
PLDI 2011, San Jose, CA, USA, June 4-8, 2011,
editorpersonMary W. Hall and
personDavid A. Padua (Eds.). publisherACM,

authorpersonPerdita Stevens.
booktitleA Landscape of Bidirectional Model
publisherSpringer Berlin Heidelberg,
addressBerlin, Heidelberg, pages408–424.

authorpersonJanis Voigtländer.
Bidirectionalization for Free! (Pearl). In
booktitleProceedings of the 36th Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (Savannah, GA, USA)
(seriesPOPL '09). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

authorpersonJanis Voigtländer.
Bidirectionalization for free! (Pearl). In
booktitleProceedings of the 36th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA,
USA, January 21-23, 2009, editorpersonZhong Shao
and personBenjamin C. Pierce (Eds.).
publisherACM, pages165–176.

authorpersonJanis Voigtländer.
Ideas for connecting inductive program synthesis
and bidirectionalization, See DBLP:conf/pepm/2012,

[Voigtländer, Hu, Matsuda, and
WangVoigtländer et al2013]
authorpersonJanis Voigtländer,
personZhenjiang Hu, personKazutaka Matsuda, and
personMeng Wang. year2013.
Enhancing semantic bidirectionalization via shape
bidirectionalizer plug-ins.
journalJ. Funct. Program. volume23,
number5 (year2013), pages515–551.

authorpersonPhilip Wadler.
Theorems for Free!. In
booktitleProceedings of the fourth international conference
on Functional programming languages and computer architecture, FPCA 1989,
London, UK, September 11-13, 1989,
editorpersonJoseph E. Stoy (Ed.).
publisherACM, pages347–359.

authorpersonPhilip Wadler.
Deforestation: Transforming Programs to Eliminate
journalTheor. Comput. Sci. volume73,
number2 (year1990), pages231–248.

[Yamaguchi, Matsuda, David, and WangYamaguchi
et al2021]
authorpersonMasaomi Yamaguchi,
personKazutaka Matsuda, personCristina David, and
personMeng Wang. year2021.
Synbit: Synthesizing Bidirectional Programs
using Unidirectional Sketches.
journalCoRR  volumeabs/2108.13783

[Yokoyama, Axelsen, and GlückYokoyama
et al2008]
authorpersonTetsuo Yokoyama,
personHolger Bock Axelsen, and personRobert
Glück. year2008.
Principles of a reversible programming language.
In booktitleProceedings of the 5th Conference on Computing
Frontiers, 2008, Ischia, Italy, May 5-7, 2008,
editorpersonAlex Ramírez,
personGianfranco Bilardi, and personMichael
Gschwind (Eds.). publisherACM, pages43–54.

[Yokoyama, Axelsen, and GlückYokoyama
et al2011]
authorpersonTetsuo Yokoyama,
personHolger Bock Axelsen, and personRobert
Glück. year2011.
Towards a Reversible Functional Language. In
booktitleRC (seriesLecture Notes in
Computer Science, Vol. volume7165),
editorpersonAlexis De Vos and
personRobert Wille (Eds.). publisherSpringer,

§ APPENDIX

§.§ Full Definition of Typing Relation

The complete definition of (our fragment of) HOBiT's typing relation is given in Fig. <ref>.
The definition assumes constructors have simple types $\con{C} : A_1 \to \dots \to A_n \to A$, which
may be instantiation results of their (rank-1) polymorphic types (such as list constructors $(:)$ and $[\,]$).

$\Gamma; \Delta \vdash e : A$

\begin{gather*}
\infer
{ \Gamma; \Delta \vdash x : A  }
{ \Gamma(x) = A }
\quad
\infer
{ \Gamma; \Delta \vdash x : \BX{\tau}}
{ \Delta(x) = \tau }
\quad
\infer
{ \Gamma; \Delta \vdash \lambda x.e : A \to B }
{ \Gamma, x:A; \Delta \vdash e : B }
\quad
\infer
{ \Gamma; \Delta \vdash e_1 \A e_2 : B }
{ \Gamma; \Delta \vdash e_1 : A \to B
\quad
\Gamma; \Delta \vdash e_2 : A }
\\
\infer
{\Gamma; \Delta \vdash \con{C} \A \V{e}: A }
{ \{ \Gamma; \Delta \vdash e : A_i \}_i \quad \con{C} : A_1 \to \dots \to A_n \to A   }
% \quad
% \infer
% {\Gamma; \Delta \vdash \con{False} : \con{Bool}}
% {}
% \quad
% \infer
% {\Gamma; \Delta \vdash [\,] : [A]}
% {}
% \quad
% \infer
% { \Gamma; \Delta \vdash (e_1 : e_2) : [A] }
% { \Gamma; \Delta \vdash e_1 : A
% \quad
% \Gamma; \Delta \vdash e_2 : [A]
% }
\quad
\infer
{ \Gamma; \Delta \vdash \CASE~e_0~\OF~\{ p_i \to e_i \}_i : B }
{ \Gamma; \Delta \vdash e_0  : A
\quad
\{ \Gamma_i \vdash p_i : A \quad \Gamma, \Gamma_i ; \Delta \vdash e_i : B \}_i
\\
\infer
{ \Gamma ; \Delta \vdash \LIFTU{e} : \BX{\tau} }
{ \Gamma ; \Delta \vdash e : \tau }
\quad
\infer
{ \Gamma ; \Delta \vdash \bxcon{C} \A \V{e}: \BX{\tau} }
{ \{ \Gamma; \Delta \vdash e_i : \BX{\tau_i} \}_i
\quad
\con{C} : \tau_1 \to \dots \to \tau_n \to \tau
% \infer
% {\Gamma; \Delta \vdash \bx{\con{True}} : \BX{\con{Bool}}}
% {}
% \quad
% \infer
% {\Gamma; \Delta \vdash \bx{\con{False}} : \BX{\con{Bool}}}
% {}
% \quad
% \infer
% {\Gamma; \Delta \vdash \bx{[\,]} : \BX{[\tau]}}
% {}
% \quad
% \infer
% { \Gamma; \Delta \vdash (e_1 \mathbin{\bx{:}} e_2) : \BX{[\tau]} }
% { \Gamma; \Delta \vdash e_1 : \BX{\tau}
%   \quad
%   \Gamma; \Delta \vdash e_2 : \BX{[\tau]}
% }
\\
\infer
{ \Gamma; \Delta \vdash \BCASE~e_0~\BOF~\{ {{p_i}} \to e_i~\BWITH~e'_i~\BBY~e''_i \}_i : \BX{\sigma} }
{ \Gamma; \Delta \vdash e_0 : \BX{\tau}
\quad
\{ \Delta_i \vdash p_i : A \quad \Gamma ; \Delta, \Delta_i \vdash e_i : B \quad \Gamma; \Delta \vdash e'_i : \sigma \to \con{Bool} \quad \Gamma; \Delta \vdash e''_i : \tau \to \sigma \to \tau  \}_i
\end{gather*}

$\Gamma \vdash p : A$

\begin{gather*}
\infer
{ x: A \vdash x : A }
\quad
\infer
{\Gamma_1,\dots,\Gamma_n \vdash \con{C} \A \V{p} : A  }
{ \{ \Gamma_i \vdash p_i : A_i \}
\quad
\con{C} : A_1 \to \dots \to A_n \to A
% \infer
% { \emptyset \vdash \con{True} : \con{Bool} }
% {}
% \quad
% \infer
% { \emptyset \vdash \con{False} : \con{Bool} }
% {}
% \quad
% \infer
% { \emptyset \vdash [\,] : [A] }
% { }
% \quad
% \infer
% { \Gamma_1,\Gamma_2 : (e_1 : e_2) : [A] }
% { \Gamma_1 \vdash e_1 : A
% \quad
% \Gamma_2 \vdash e_2 : [A] }
\end{gather*}

$\Gamma \vdash P$

\begin{gather*}
\infer
{ \Gamma \vdash f_1 = e_1; \dots ; f_n = e_n  }
{ \{ \Gamma ; \emptyset \vdash e_i : \Gamma(f_i) \}_{i} }
\end{gather*}

Typing rules: $\Delta \vdash p : \sigma$ is defined similarly to $\Gamma \vdash p : A$ but asserts that the resulting environment is actually an bidirectional one and every type that occurs in the derivation is a $\sigma$-type.

§.§ Full Definition of Sketch Generation Rules

Figure <ref> provides the sketch generation rules used in Section <ref>.

For simplicity of presentation, in Section <ref> we did not explicitly capture the type of the code to be generated in the specialized holes as it can be recovered from the sketch and typing environment $\Gamma$. However, here we make it explicit by augmenting
both the exit condition hole and the reconciliation hole with
the typing environment $\Gamma$ and the type of the code to be
synthesized: $\EHole{\Gamma}{\sigma \to \con{Bool}}{e}$ and
$\RHole{\Gamma}{\sigma_0 \to \sigma \to \sigma_0}{p}{e}$.

\begin{gather*}
\ninfer
{ \GenTmp{\Gamma'}{\Delta'}{\BX{\tau}}{\Gamma}{e}{\tau}{\LIFTU{e'}} }
{ \GenTmp{\Gamma'}{\Delta'}{\tau}{\Gamma}{e}{\tau}{e'} }
\quad
\ninfer
{ \GenTmp{\Gamma'}{\Delta'}{A'}{\Gamma}{x}{A}{x}}
{ x:A\in\Gamma\quad x:A'\in\Gamma' }
\quad
\ninfer
{ \GenTmp{\Gamma'}{\Delta'}{\BX{\sigma}}{\Gamma}{x}{\sigma}{x} }
{ x:\sigma\in\Gamma\quad x:\sigma\in\Delta' }
\\
\ninfer
{ \GenTmp{\Gamma'}{\Delta'}{(A_1'\to A_2')}{\Gamma}{\lambda x.e}{A_1\to A_2}{\lambda x.e'} }
{ \GenTmp{(\Gamma',x:A_1')}{\Delta'}{A_2'}{(\Gamma,x:A_1)}{e}{A_2}{e'} }
\\
\ninfer
{ \GenTmp{\Gamma'}{\Delta'}{A'}{\Gamma}{e_1 \A e_2}{A}{e_1' \A e_2'} }
{ \begin{tarray}{c}
\GenTmp{\Gamma'}{\Delta'}{(A_2'\to A')}{\Gamma}{e_1}{(A_2\to A)}{e_1'} \quad
A_2 \leadsto B_2 \quad
\GenTmp{\Gamma'}{\Delta'}{B_2}{\Gamma}{e_2}{A_2}{e_2'}
\end{tarray}
\\
\ninfer
\GenTmp{\Gamma'}{\Delta'}{A}{\Gamma}{\con{C} \A \V{e}}{A}{\con{C} \A \V{e'}}
\con{C} : A_1 \to \dots \to A_n \to A \quad
\{ \GenTmp{\Gamma'}{\Delta'}{A_i}{\Gamma}{e_i}{A_i}{e'_i}  \}_i
\\
\ninfer
\GenTmp{\Gamma'}{\Delta'}{\BX{\tau}}{\Gamma}{\con{C} \A \V{e}}{\tau}{\bxcon{C} \A \V{e'}}
\con{C} : \tau_1 \to \dots \to \tau_n \to \tau \quad
\{ \GenTmp{\Gamma'}{\Delta'}{\BX{\tau_i}}{\Gamma}{e_i}{\tau_i}{e'_i}  \}_i
\\
\ninfer
{ \GenTmp{\Gamma'}{\Delta'}{A'}{\Gamma}{\CASE~e_0~\OF~\{ p_i \to e_i \}_i}{A}{\CASE~e_0'~\OF~\{ p_i \to e_i' \}_i} }
{ \begin{tarray}{c}
\GenTmp{\Gamma'}{\Delta'}{A_0'}{\Gamma}{e_0}{A_0}{e_0'} \quad
A_0 \leadsto A_0' \\
\{ \Gamma_i\vdash p_i: A_0 \quad
\Gamma'_i \vdash p_i : A_0' \quad
\GenTmp{(\Gamma',\Gamma_i')}{\Delta'}{A'}{(\Gamma,\Gamma_i)}{e_i}{A}{e_i'}  \}_i
\end{tarray} }
\\
\ninfer
{ \GenTmp{\Gamma'}{\Delta'}{\BX{\sigma}}{\Gamma}{\CASE~e_0~\OF~\{ p_i \to e_i \}_i}{\sigma}{\BCASE~e_0'~\BOF
\left\{\begin{tarray}{l}
\displaystyle \bx{{p_i}} \to e_i'                                         \\
\displaystyle \BWITH~\EHole{\Gamma'}{\sigma \to \con{Bool}}{e_i'} \\
\displaystyle \BBY~\RHole{\Gamma'}{\sigma_0 \to \sigma \to \sigma_0}{p_i}{e_i}
\end{tarray}\right\}_i}}
{ \begin{tarray}{c}
\GenTmp{\Gamma'}{\Delta'}{\BX{\sigma_0}}{\Gamma}{e_0}{\sigma_0}{e_0'} \\
\{\Gamma_i\vdash p_i: \sigma_0 \quad
\Delta'_i \vdash p_i : \sigma_0 \quad
\GenTmp{\Gamma'}{(\Delta',\Delta_i')}{\BX{\sigma}}{(\Gamma,\Gamma_i)}{e_i}{\sigma}{e_i'}
\end{tarray} }
\end{gather*}

Sketch generation rules for expressions

Discussion on -polymorphism

supports $\LET$-polymorphism as illustrated by some $\GET$ programs used in the experiments (Section <ref>), such as $\var{append} :: [a] \to [a] \to [a]$ and $\var{reverse} :: [a] \to [a]$ that have polymorphic types.
However, for simplicity, we assumed simple types in our formal development (, Fig. <ref> and <ref>).

The handling of bidirectional programs with (rank 1) polymorphic types is mostly straightforward. For example, for the sketch generation in Fig. <ref>,
we can leverage the fact that in the standard typing system for $\LET$ polymorphism <cit.>, expressions can only have monomorphic types.
As a consequence, we can say $A$ and $A$' in $\GenTmp{\Gamma'}{\Delta'}{A'}{\Gamma}{e}{A}{e'}$ are always monomorphic.
Also, these types $A$ and $A$' are fully determined in advance of the generation,
because $A$ comes from the typing derivation of the original $\GET$ program and $A'$ is obtained form $A$ by inserting $\BX{}$. The types $A$ and $A$' may contain
type variables but they are rigid (, not subject to unification).
Note that we can access to the typing derivation of the original $\GET$ program as well as the code itself.

Though it is still straightforward, a slightly more careful discussion is needed for the type-directed generation of terms to fill shape-restricted holes (Section <ref>), where types being used for type-directed generation may not be immediately clear.
In an extreme case, for example, if the component functions contains $\var{const} :: a \to b \to a$, we have no immediate information of the type
to generate its second argument as it cannot be determined by instantiation of $a$.
This suggests that we may need to consider explicit handing of type variables and unification
in the term generation, which complicates the system.

Fortunately though, our back-end system for (lazy) nondeterministic generation is powerful enough to address the issue without introducing any additional complication;
in the system, a logic (, unifiable) variable (, (non-rigid) type variable) can be expressed by
nondeterministic generation of all the things (, monomorphic types) to substitute for it,
and by the $\var{share}$ operator <cit.>.

§.§ Full Definition of Filtering based on Branch Traces

§.§.§ Formal Semantics of HOBiT

To understand definition of filtering based on branch traces, one needs to know the formal semantics of HOBiT.
The semantics of HOBiT is defined so that a term-in-context $\emptyset; \Delta \vdash e : \BX{\sigma}$ defines a bidirectional transformation between $\Delta$ and $\sigma$.
However, it is not clear how to interpret function abstractions and applications to achieve this goal.
Thus, HOBiT adopts the staged semantics; it first evaluates $\lambda$s away to obtain a first-order residual expression $E$ from $e$, and
then interprets $E$ as a bidirectional transformation between $\Delta$ and $\sigma$.
Specifically, we use three evaluation relations:
$\EvalRelU{e}{v}$ is for unidirectional evaluation to obtain residual expressions, and
$\EvalRelF{\mu}{E}{u}$ and $\EvalRelB{\mu}{E}{u}{\mu'}$ for bidirectional evaluation of residual expressions.

Values $v$, residual expressions $E$ and first-order values $u$ are defined as follows.

\[
\begin{tarray}{lcll}
v &::=& \con{True} \mid \con{False} \mid [\,] \mid v_1 : v_2 \mid \lambda x.e \mid E \\
E &::=& x \mid  \bx{\con{True}} \mid \bx{\con{False}} \mid \bx{[\,]} \mid E_1 \mathbin{\bx{:}} E_2 \mid \CASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~v'_i~\BY~v''_i \}_i \mid \LIFTU{u} \\
u &::=& \con{True} \mid \con{False} \mid [\,] \mid u_1 : u_2
\end{tarray}
\]

Intuitively, $v$, $E$, and $u$ represent evaluation results of $A$-, $\BX{\tau}$-, and $\tau$-typed expressions, respectively.
Note that $e$/$e_i$ appears under $\lambda$ or $\CASE$, meaning that their evaluates are delayed.

\begin{gather*}
\infer
\quad
\infer
{(f = e) \in P \quad \EvalRelU{e}{v}}
\quad
\infer
{\EvalRelU{e_1 \A e_2}{v}}
{\EvalRelU{e_1}{\lambda x.e} \quad
\EvalRelU{e_2}{v_2} \quad
\EvalRelU{e[v_2/x]}{v}
\quad
\infer
{\EvalRelU{\lambda x.e}{\lambda x.e}}
\\
\infer
\EvalRelU{\CASE~e_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~e'_i~\BY~e''_i \}_i}{\CASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~v'_i~\BY~v''_i \}_i}
\EvalRelU{e_0}{E_0} \quad
\{ \EvalRelU{e'_i}{v'_i} \quad \EvalRelU{e''_i}{v''_i} \}_i
% \quad
% \text{$\fv(p_i)$: fresh}
\end{gather*}

Unidirectional Evaluation Rules (Excerpt)

Unidirectional evaluation The rules for the unidirectional evaluation relation is rather standard, as excerpted in Fig. <ref>.
The bidirectional constructs (, bidirectional constructors and bidirectional $\CASE$) are frozen, , treated as
ordinary constructors in this evaluation.

Bidirectional ($\GET$ and $\PUT$) evaluation relations
The $\GET$ and $\PUT$ evaluation relations, $\EvalRelF{\mu}{E}{u}$ and $\EvalRelB{\mu}{E}{u}{\mu'}$,
are defined so that they form a bidirectional transformation.
A caveat here is that the $\PUT$ evaluation relation returns an environment of which domain is $\fv(E)$.

\[
\begin{array}{c@{\quad}c@{\quad}c@{\quad}c}
\displaystyle
\infer
{\EvalRelF{\mu}{x}{\mu(x)} }
%  &
% \displaystyle
% \infer
% { \EvalRelF{\mu}{\bx{c}}{c} }
% { c = \con{True}, \con{False}, [\,] }
\displaystyle
\infer
{ \EvalRelF{\mu}{\bxcon{C} \A \V{e}}{ \con{C} \A \V{u} } }
{ \{ \EvalRelF{\mu}{e_i}{u_i} \}_i }
\displaystyle
\infer
{ \EvalRelF{\mu}{ \LIFTU{u} }{ u } }
{ }
\\[10pt]
\displaystyle
\infer
{\EvalRelB{\mu}{x}{u}{ \{x = u\} } }
%  &
% \displaystyle
% \infer
% { \EvalRelB{\mu}{\bx{c}}{c}{ \emptyset }  }
% { c = \con{True}, \con{False}, [\,] }
\displaystyle
\infer
{ \EvalRelB{\mu}{ \bxcon{C} \A \V{e} }{ \con{C} \A \V{u} }{\textstyle \bigcurlyvee \mu'_i} }
{ \{\EvalRelB{\mu}{e_i}{u_i}{\mu'_i}\}_i }
\displaystyle
\infer
{ \EvalRelB{\mu}{ \LIFTU{u} }{ u }{\emptyset} }
{  }
\end{array}
\]

$\GET$ and $\PUT$ Evaluation Rules (except $\CASE$)

Most $\GET$ and $\PUT$ evaluation rules are straightforward except $\CASE$ (Fig. <ref>).
In the definition, we use the merging operator $\lub$ defined as: $\mu_1 \lub \mu_2 = \mu_1 \cup \mu_2$ if
there is no $x$ such that $\mu(x) \ne \mu'(x)$.

The most interesting rules are those for $\CASE$. In the $\GET$ direction, the evaluation rule is similar to the ordinary one
except that it involves runtime check of exit conditions.

\[
\infer
{ \EvalRelF{\mu}{\CASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~v'_i~\BY~v''_i \} }{ u } }
\EvalRelF{\mu}{E_0}{u_0} \quad
\sem{p_i}\A u_0 = \mu_i \quad
\EvalRelU{e_i}{E_i} \quad
\EvalRelF{\mu \uplus \mu_i}{E_i}{u} \quad
\EvalRelU{v'_i \A u}{\con{True}}
\]

Here, we write $\sem{p}$ for the semantics of pattern matching by $p$: , $\sem{p} \A u$ is a partial function that returns a binding $\mu$
with $\dom(\mu) = \fv(p)$ and $u = p\mu$ if exists (and fails otherwise), where we identity an environment $\mu$ and a substitution.
For this case (even after extension with guards), $\sem{p}$ is injective and thus has a left inverse $\sem{p}^{-1}$, which will be used by the $\PUT$ evaluation of $\CASE$.
The rule implicitly assumes that $\dom(\mu_i)$ (, $\fv(p_i)$) and $\dom(\mu)$ are disjoint;
we assume appropriate $\alpha$-renaming that is consistent in $\GET$ and $\PUT$ to fulfill the condition.
Reconciliation functions are not used at all in the $\GET$ direction.

There are two $\PUT$ evaluation rules for $\CASE$: one is for when there is no branch switching and the other is for when branch switching happens.
We first explain the non-branch-switching one.

\[
\infer
{ \EvalRelB{\mu}{\CASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~v'_i~\BY~v''_i \} }{ u }{ \mu'_0 \lub \mu' } }
\begin{array}{c}
\EvalRelF{\mu}{E_0}{u_0} \quad
\sem{p_i}\A u_0 = \mu_i \quad
\EvalRelU{v'_i \A u}{\con{True}} \\
\EvalRelU{e_i}{E_i} \quad
\EvalRelB{\mu \uplus \mu_i}{E_i}{u}{\mu' \uplus_{\dom(\mu),\dom(\mu_i)} \mu'_i} \quad
\sem{p_i}^{-1} \A (\mu'_i \triangleleft \mu_i) = u_0' \quad
\EvalRelB{\mu}{E_0}{u'_0}{\mu'_0}
\end{array}
\]

Intuitively, the rule says that we use the original branch if its associated exit condition $v'_i$ becomes $\con{True}$ for an updated value $u$.
In this step, we need to separate the backward evaluation result of $E_i$ into two: $\mu'$ for free variables in $E_i$ and $\mu'_i$ for variables introduced by $p_i$.
To express the separation, this rule uses $\mu_1 \uplus_{X,Y} \mu_2$ which behaves similarly to $\mu_1 \uplus \mu_2$, while also ensuring that $\dom(\mu_1) \subseteq X$ and $\dom(\mu_2) \subseteq Y$.
A caveat here is that some $p_i$ variables may not occur in $E_i$, and for such a case $\dom(\mu'_i)$ is strictly smaller than $\fv(p_i)$ ($= \dom(\mu_i)$);
, we may not be ready to apply $\sem{p_i}^{-1}$ that assumes environments with the domain $\fv(p_i)$.
Thus, to apply $\sem{p_i}^{-1}$, the rule uses the operator $\triangleleft$ (read “defaulting by”) defined by:

\[
(\mu \triangleleft \mu')(x) = \begin{cases}
\mu(x)  & \text{if}~x \in \dom(\mu)                      \\
\mu'(x) & \text{if}~x \in \dom(\mu') \setminus \dom(\mu)
\end{cases}
\]

Once the rule applies $\sem{p_i}^{-1}$ to compute an updated value $u'_0$ of $E_0$, it performs the backward evaluation of $E_0$ to obtain $\mu'_0$ and then results in $\mu'_0 \lub \mu'$.
Again, reconciliation functions have no use in this case.

The branch-switching $\PUT$ rule handles the case where the original exit condition becomes $\con{False}$ for an updated value $u$.

\[
\infer
{ \EvalRelB{\mu}{\CASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~v'_i~\BY~v''_i \} }{ u }{ \mu'_0 \lub \mu' } }
\begin{array}{c}
\EvalRelF{\mu}{E_0}{u_0} \quad
\sem{p_i}\A u_0 = \mu_i \quad
\EvalRelU{v'_i \A u}{\con{False}} \quad
\EvalRelU{v'_j \A u}{\con{True}} \quad
\{ \EvalRelU{v'_k \A u}{\con{False}} \}_{k < j}
\\
\EvalRelU{v''_j \A u_0 \A u}{u_0^\mathrm{rec}} \quad
\sem{p_j} \A u_0^\mathrm{rec} = \mu_j
\\
\EvalRelU{e_j}{E_j} \quad
\EvalRelB{\mu \uplus \mu_j}{E_j}{u}{\mu' \uplus_{\dom(\mu),\dom(\mu_j)} \mu'_j} \quad
\sem{p_j}^{-1} \A (\mu'_j \triangleleft \mu_j) = u_0' \quad
\EvalRelB{\mu}{E_0}{u'_0}{\mu'_0}
\end{array}
\]

Then, the rule chooses the branch $j$ of which exit condition becomes $\con{True}$ first (, the first match principle).
We now want to perform the backward evaluation of $E_j$, but this is not immediately possible as we do not know the original environment due to $p_j$.
Pattern-matching with $u_0$ is a non solution as it matches $p_i$ and not likely to match $p_j$.
Thus, we use the associated reconciliation function $v''_j$ to construct a reconciled result $u_0^\mathrm{rec}$ to be matched with $p_j$.
The rest of the behavior is the same as the non-branch switching case.

Here, we provide details on the filtering based on branch traces, corresponding to Section <ref>.

A trace is a tree that preserves information about which branches of $\BCASE$ were chosen during the $\GET$ or $\PUT$ evaluation.
The syntax of such a trace is as follows:

\[\revised{\mathit{tr}  ::= \epsilon \mid \mathrm{Br}(\mathit{tr}_0,j,\mathit{tr}_1) \mid [\mathit{tr}_1,\ldots,\mathit{tr}_n]}
\]

Here, $\mathrm{Br}(\mathit{tr}_0,j,\mathit{tr}_1)$ is a trace for
$\BCASE~E_0~\BOF~\{ p_i \rightarrow e_i~\WITH~v_i'~\BY~v_i''\}_i$, where $\mathit{tr}_0$ is the trace for $E_0$,
$j$ stands for the $j$-th branch that was chosen, and $\mathit{tr}_1$ is the trace for $E_j$.
The traces $\mathit{tr}_1,\ldots,\mathit{tr}_n$ in
$[\mathit{tr}_1,\ldots,\mathit{tr}_n]$ correspond to the arguments of a constructor application $\bxcon{C} \A e_1 \A ,\ldots, \A e_n$. We abbreviate $[\mathit{tr}_1,\ldots,\mathit{tr}_n]$ to $\V{\mathit{tr}}$ when $n$ is obvious.

Primer on HOBiT's formal semantics
To understand the definition of filtering based on branch traces, one needs to know the formal semantics of HOBiT.
The semantics of HOBiT is defined so that a term-in-context $\emptyset; \Delta \vdash e : \BX{\sigma}$ defines a bidirectional transformation between $\Delta$ and $\sigma$.
However, it is not clear how to interpret function abstractions and applications to achieve this goal.
Thus, HOBiT adopts the staged semantics; it first evaluates $\lambda$s away to obtain a first-order residual expression $E$ from $e$, and
then interprets $E$ as a bidirectional transformation between $\Delta$ and $\sigma$.
Specifically, we use three evaluation relations:
$\EvalRelU{e}{v}$ is for unidirectional evaluation to obtain residual expressions, and
$\EvalRelF{\mu}{E}{u}$ and $\EvalRelB{\mu}{E}{u}{\mu'}$ for bidirectional evaluation of residual expressions.

Values $v$, residual expressions $E$ and first-order values $u$ are defined as follows.

\[
\begin{tarray}{lcll}
v &::=& \con{True} \mid \con{False} \mid [\,] \mid v_1 : v_2 \mid \lambda x.e \mid E \\
E &::=& x \mid  \bx{\con{True}} \mid \bx{\con{False}} \mid \bx{[\,]} \mid E_1 \mathbin{\bx{:}} E_2 \mid \CASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~v'_i~\BY~v''_i \}_i \mid \LIFTU{u} \\
u &::=& \con{True} \mid \con{False} \mid [\,] \mid u_1 : u_2
\end{tarray}
\]

Intuitively, $v$, $E$, and $u$ represent evaluation results of $A$-, $\BX{\tau}$-, and $\tau$-typed expressions, respectively.

For more details on HOBiT, please see HOBiT's original paper <cit.>.

's evaluation rules with traces
The rules for the unidirectional evaluation relation are rather standard, as excerpted in Fig. <ref>.
The bidirectional constructs (, bidirectional constructors and bidirectional $\CASE$) are frozen, , treated as
ordinary constructors in this evaluation.

For filtering based on trace branches we make use of the evaluation relations $\EvalRelFT{\mu}{E}{u}{\mathit{tr}}$ and $\EvalRelBT{\mu}{E}{u}{\mathit{tr}}{\mu'}$,
defined by the rules in Fig. <ref>.
Intuitively, $\EvalRelFT{\mu}{E}{v}{\mathit{tr}}$ means that a program $E$ is reduced to the original view $v$ under the the original source environment $\mu$ through a trace $\mathit{tr}$.

Accordingly, $\EvalRelBT{\mu}{E}{v}{\mathit{tr}}{\mu'}$ means that a program $E$ is evaluated according to its $\PUT$ behavior such that the
updated source $\mu'$ is obtained from the the original source $\mu$ and the updated view $v$ through a trace $\mathit{tr}$.

These traced evaluation relations only differ from the original $\GET$ and $\PUT$ evaluation relations <cit.> in reference to traces.
Thus, we omit the definitions of the original, untraced evaluation relations $\EvalRelF{\mu}{E}{u}$ and $\EvalRelB{\mu}{E}{u}{\mu'}$, whereas
they appear in Fig. <ref>.

In the evaluation rules, we write $\sem{p}$ for the semantics of pattern matching by $p$: , $\sem{p} \A u$ is a partial function that returns a binding $\mu$
with $\dom(\mu) = \fv(p)$ and $u = p\mu$ if such $\mu$ exists (and fails otherwise).
In HOBiT, $\sem{p}$ is injective and thus has a left inverse $\sem{p}^{-1}$.
The rules for $\BCASE$ (, Tg-BCase, Tp-BCase1, and Tp-BCase2) implicitly assume that $\dom(\mu_i)$ (, $\fv(p_i)$) and $\dom(\mu)$ are disjoint;
we assume appropriate $\alpha$-renaming that is consistent in $\GET$ and $\PUT$ to fulfill the condition.
To separate environments, the evaluation rules use $\mu_1 \uplus_{X,Y} \mu_2$ which behaves similarly to $\mu_1 \uplus \mu_2$, while also ensuring $\dom(\mu_1) \subseteq X$ and $\dom(\mu_2) \subseteq Y$.
The operator $\triangleleft$ is defined by:

\[
(\mu' \triangleleft \mu)(x) = \begin{cases}
\mu'(x)  & \text{if}~x \in \dom(\mu')                      \\
\mu(x) & \text{if}~x \in \dom(\mu) \setminus \dom(\mu')
\end{cases}
\]

The operator $\lub$ is defined as: $\mu_1 \lub \mu_2 = \mu_1 \cup \mu_2$ if $\mu_1(x) = \mu_2(x)$ for all $x \in \dom(\mu_1) \cap \dom(\mu_2)$,
and otherwise $\mu_1 \lub \mu_2$ is undefined.

\begin{gather*}
\infer
\quad
\infer
{(f = e) \in P \quad \EvalRelU{e}{v}}
\quad
\infer
{\EvalRelU{e_1 \A e_2}{v}}
{\EvalRelU{e_1}{\lambda x.e} \quad
\EvalRelU{e_2}{v_2} \quad
\EvalRelU{e[v_2/x]}{v}
\quad
\infer
{\EvalRelU{\lambda x.e}{\lambda x.e}}
\\
\infer
\EvalRelU{\CASE~e_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~e'_i~\BY~e''_i \}_i}{\CASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~v'_i~\BY~v''_i \}_i}
\EvalRelU{e_0}{E_0} \quad
\{ \EvalRelU{e'_i}{v'_i} \quad \EvalRelU{e''_i}{v''_i} \}_i
% \quad
% \text{$\fv(p_i)$: fresh}
\end{gather*}

Unidirectional evaluation rules (excerpt)

\begin{gather*}
\begin{array}{c@{\quad}c@{\quad}c@{\quad}c}
\displaystyle
\ninfer{Tg-Var}
{\EvalRelFT{\mu}{x}{\mu(x)}{\TrNil} }
%  &
% \displaystyle
% \infer
% { \EvalRelFT{\mu}{\bx{c}}{c}{\TrNil} }
% { c = \con{True}, \con{False}, [\,] }
\displaystyle
\ninfer{Tg-BCon}
{ \EvalRelFT{\mu}{\bxcon{C} \A \V{e}}{\con{C} \A \V{u}}{\V{\mathit{tr}}} }
{ \{\EvalRelFT{\mu}{e_i}{u_i}{\mathit{tr}_i} \}_i}
\displaystyle
\ninfer{Tg-!}
{ \EvalRelFT{\mu}{ \LIFTU{u} }{ u }{\TrNil} }
{ }
\\[10pt]
\displaystyle
\ninfer{Tp-Var}
{\EvalRelBT{\mu}{x}{u}{\TrNil}{ \{x = u\} } }
%  &
% \displaystyle
% \infer
% { \EvalRelBT{\mu}{\bx{c}}{c}{\TrNil}{ \emptyset }  }
% { c = \con{True}, \con{False}, [\,] }
\displaystyle
\ninfer{Tp-BCon}
{ \EvalRelBT{\mu}{ \bxcon{C} \A \V{e} }{ \con{C} \A \V{u} }{\V{\mathit{tr}}}{\bigcurlyvee \mu'_i } }
{ \{\EvalRelBT{\mu}{e_i}{u_i}{\mathit{tr}_i}{\mu'_i}\}_i }
\displaystyle
\ninfer{Tp-!}
{ \EvalRelBT{\mu}{ \LIFTU{u} }{ u }{\TrNil}{\emptyset} }
{  } \\[10pt]
\end{array}\\
\ninfer{Tg-BCase}
{ \EvalRelFT{\mu}{\BCASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\BWITH~v'_i~\BBY~v''_i \} }{ u }{ \TrBranch{\mathit{tr}_0}{i}{\mathit{tr}_i} } }
\EvalRelFT{\mu}{E_0}{u_0}{\mathit{tr}_0} \quad
\sem{p_i}\A u_0 = \mu_i \quad
\EvalRelU{e_i}{E_i} \quad
\EvalRelFT{\mu \uplus \mu_i}{E_i}{u}{\mathit{tr}_i} \quad
\EvalRelU{v'_i \A u}{\con{True}}
\ninfer{Tp-BCase1}
{ \EvalRelBT{\mu}{\BCASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\BWITH~v'_i~\BBY~v''_i \} }{ u }{ \TrBranch{\mathit{tr}_0}{i}{\mathit{tr}_i} }{ \mu'_0 \lub \mu' } }
\begin{array}{c}
\EvalRelF{\mu}{E_0}{u_0} \quad
\sem{p_i}\A u_0 = \mu_i \quad
\EvalRelU{v'_i \A u}{\con{True}} \\
\EvalRelU{e_i}{E_i} \quad
\EvalRelBT{\mu \uplus \mu_i}{E_i}{u}{\mathit{tr}_i}{\mu' \uplus_{\dom(\mu),\dom(\mu_i)} \mu'_i} \quad
\sem{p_i}^{-1} \A (\mu'_i \triangleleft \mu_i) = u_0' \quad
\EvalRelBT{\mu}{E_0}{u'_0}{\mathit{tr}_0}{\mu'_0}
\end{array}
\ninfer{Tp-BCase2}
{ \EvalRelBT{\mu}{\BCASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\BWITH~v'_i~\BBY~v''_i \} }{ u }{ \TrBranch{\mathit{tr}_0}{j}{\mathit{tr}_i} }{ \mu'_0 \lub \mu' } }
\begin{array}{c}
\EvalRelF{\mu}{E_0}{u_0} \quad
\sem{p_i}\A u_0 = \mu_i \quad
\EvalRelU{v'_i \A u}{\con{False}} \quad
\EvalRelU{v'_j \A u}{\con{True}} \quad
\{ \EvalRelU{v'_k \A u}{\con{False}} \}_{k < j}
\\
\EvalRelU{v''_j \A u_0 \A u}{u_0^\mathrm{rec}} \quad
\sem{p_j} \A u_0^\mathrm{rec} = \mu_j
\\
\EvalRelU{e_j}{E_j} \quad
\EvalRelBT{\mu \uplus \mu_j}{E_j}{u}{ \mathit{tr}_i }{\mu' \uplus_{\dom(\mu),\dom(\mu_j)} \mu'_j} \quad
\sem{p_j}^{-1} \A (\mu'_j \triangleleft \mu_j) = u_0' \quad
\EvalRelBT{\mu}{E_0}{u'_0}{ \mathit{tr}_0 }{\mu'_0}
\end{array}
\end{gather*}

$\GET$ and $\PUT$ evaluation rules with traces

For illustration, we use $\var{appendB}$, and assume the following example was given as the backward behavior:

\[
\texttt{:put} \A (\var{uncurryB}~ \var{appendB}) \A ([1,2,3], [4,5]) \A [6,2]  = ([6,2], [\,])
\]

The trace of

\[
\texttt{:get} \A (\var{uncurryB}~ \var{appendB}) \A ([6,2], [\,])  = [6,2]
\]

and the trace of the above $\texttt{:put}$ must coincide.

The trace of this $\texttt{:get}$ (after evaluating $\var{uncurryB}$) is obtained as follows:

\[ \EvalRelFT{\{\var{xs} = [6,2], \var{ys} = [\,]\}}{\var{appendBbody}}{[6,2]}{\mathrm{Br}(\epsilon,1,[\epsilon,\mathrm{Br}(\epsilon,1,[\epsilon,\mathrm{Br}(\epsilon,0,\epsilon)])])}\]

appendBbody =  xs
[ ]      →ys      const True      λ.λ.  [ ]

a : x     →a : appendB x ys      not ∘null      λs.λ.  s

Here, the resulting overall trace is $\mathit{tr} = \mathrm{Br^1}(\epsilon^2,1,[\epsilon^3,\mathrm{Br^4}(\epsilon^5,1,[\epsilon^6,\mathrm{Br^7}(\epsilon^8,0,\epsilon^9)])])$ (for easy identification, we numbered the individual traces). Next, we explain how this is obtained.
The first step of the evaluation of $\GET$ is the case branch.
Since we have $\var{xs} = [6,2]$, the second branch (cons case) is chosen.
Thus, by Tg-BCase, the whole trace $\var{tr}$ has the form of $\mathrm{Br^1}(\var{tr}_2, 1, \var{tr}_3)$,
where $\var{tr}_2$ is the trace of the evaluation of $\var{xs}$, and $\var{tr}_3$ is the trace of the evaluation of $a \bxop{:} \var{appendB} \A x \A \var{ys}$ under $\{a = 6, x = [2],  \var{ys} = [\,], \dots\}$.

By Tg-Var, we have $\var{tr}_2 = \epsilon^2$, and
by Tg-BCon, we have $\var{tr}_3 = [\var{tr}_4, \var{tr}_5]$ for some trace $\var{tr}_4$ and $\var{tr}_5$.
Since $\var{tr}_4$ is the trace of the evaluation of $\var{a}$, we have $\var{tr}_4 = \epsilon^3$ by Tg-Var.
Then, we focus on $\var{tr}_5$, which is the trace of the evaluation of $\var{appendB} \A x \A \var{ys}$ under $\{x = [2], \var{ys} = [\,], \dots\}$.
Thus, we have[If we follow the evaluation rules precisely, we will evaluate $\var{appendBbody}[x/\var{xs}, \var{ys}/\var{ys}]$ with $\alpha$-renaming of $a$ and $x$ bound in $\var{appendBbody}$, which would bring further complication and thus is ignored here.]

\[
\EvalRelFT{\{\var{xs} = [2], \var{ys} = [\,], \dots\}}{\var{appendBbody}}{v_5}{\var{tr}_5}
\]

for some value $v_5$.
The second branch (cons case) is again chosen, and we obtain $\var{tr}_5 = \mathrm{Br^4}(\epsilon^5,1,[\epsilon^6,\mathit{tr}_6])$ for some trace $\mathit{tr}_6$.
Since $\var{tr}_6$ is the trace of the evaluation of $\var{appendB} \A x \A \var{ys}$ under $\{x = [\,], \var{ys} = [\,], \dots\}$, we have

\[
\EvalRelFT{\{\var{xs} = [\,], \var{ys} = [\,], \dots\}}{\var{appendBbody}}{v_6}{\var{tr}_6}
\]

for some value $v_6$.
Since we have $\var{xs} = [\,]$, the first branch (nil case) is chosen. Thus, by Tg-BCon, we have $\var{tr}_6 = \mathrm{Br^7}(\var{tr}_7, 0, \var{tr}_8)$ for some $\var{tr}_7$ and $\var{tr}_8$.
Since $\var{tr}_7$ is the trace of the evaluation of $\var{xs}$, we have $\var{tr}_7 = \epsilon^8$ by Tg-Var.
By Tg-Var, we have $\var{tr}_8 = \epsilon^9$.
As a result, the whole trace of the $\GET$ direction is computed as:

\[\mathit{tr} = \mathrm{Br^1}(\epsilon^2,1,[\epsilon^3,\mathrm{Br^4}(\epsilon^5,1,[\epsilon^6,\mathrm{Br^7}(\epsilon^8,0,\epsilon^9)])])\]

Then, we check if $\texttt{:put} \A (\var{uncurryB}~ \var{appendB}) \A ([1,2,3], [4,5]) \A [6,2] $ goes through the same trace $\mathit{tr}$ as $\GET$.

Essentially, this means that the following relation must hold:

\[
\EvalRelBT{\{\var{xs} = [1,2,3], \var{ys} = [4,5]\}}{\var{appendBbody}}{[6,2]}{\mathrm{Br}(\epsilon,1,[\epsilon,\mathrm{Br}(\epsilon,1,[\epsilon,\mathrm{Br}(\epsilon,0,\epsilon)])])}{\mu'}
\tag{\textdagger}\label{prop:goal}
\]

with $\mu' = \{ \var{xs} = [6,2], \var{ys} = [\,] \}$.
In this evaluation, we also make use of the trace to determine the rule to be applied.
For example, in the backward evaluation of $\var{appendBbody}$ above, we know from the trace that the second branch (cons case) is chosen.
Also, we know from the original environment, which maps $\var{xs}$ to $[1,2,3]$, that branch switching does not happen.
Thus, the last rule used in the evaluation must be Tp-BCase1.

Then, we need to check the following conditions that appear as the premises of the rule (we shall omit the $\GET$ evaluation of scrutinee and the obvious pattern matching as they are not relevant here).

\begin{gather*}
\EvalRelU{(\var{not} \circ \var{null}) \A [6,2]}{\con{True}}\\
\EvalRelBT{ \{a = 1, x = [2,3], \var{ys} = [4,5], \dots\} }{ a \bxop{:} \var{appendB} \A x \A \var{ys} }{ [6,2] }{\var{tr}_3}{ \mu'_1 \uplus_{\{\var{ys}, \dots\}, \{a,x\}} \mu'_2 } \tag{\ensuremath{\ast}}\label{prop:put1}\\
\EvalRelBT{ \{ \var{xs} = [1,2,3], \dots \} }{ \var{xs} }{ \sem{a : x}^{-1} (\mu_2' \triangleleft \{ a = 1, x = [2,3] \}) }{\var{tr}_2}{ \mu'_3 }\\
\mu' = \mu'_1 \lub \mu'_3
%    \EvalRelBT{ \{
\end{gather*}

Here, $\var{tr}_2, \var{tr}_3, \dots$ are the traces that appeared in the $\GET$ evaluation; hence $\var{tr}_2 = \epsilon$ and $\var{tr}_3 = [\var{tr}_4, \var{tr}_5] = [\epsilon,\mathrm{Br}(\epsilon,1,[\epsilon,\mathrm{Br}(\epsilon,0, \epsilon)])]$ for example.
The first condition clearly holds, and the third condition can be solved by Tp-Var with
$\mu'_3 = \{ \var{xs} = \sem{a : x}^{-1} (\mu_2' \triangleleft \{ a = 1, x = [2,3] \}) \}$. So, let's focus on the
second condition (<ref>).
By Tp-BCon, this condition is reduced to

\begin{gather*}
\EvalRelBT{ \{a = 1, \dots\} }{ a  }{ 6 }{\var{tr}_4}{ \mu'_4 }
\end{gather*}

and checking whether $\var{tr}_5$ is the trace of the backward evaluation of $\var{append} \A x \A \var{ys}$
under $\{ x = [2,3], \var{ys} = [4,5], \dots \}$ for the updated view $[2]$ to yield $\mu'_5$ such that $\mu'_1 \uplus_{\{\var{xs},\var{ys}\}, \{a,x\}} \mu'_2  = \mu'_4 \lub \mu'_5$.
By Tp-Var, it is easy to see that the former holds with $\mu'_4 = \{ a = 6 \}$.
The latter holds if (and only if)[Similar to Footnote <ref>.]

\[
\EvalRelBT{\{\var{xs} = [2,3], \var{ys} = [4,5], \dots \}}{\var{appendBbody}}{[2]}{\var{tr}_5}{\mu'_6}
\]

holds with $\var{tr}_5 = \mathrm{Br}(\epsilon,1,[\epsilon, \var{tr}_6]) = \mathrm{Br}(\epsilon, 1,[\epsilon,\mathrm{Br}(\epsilon,0,\epsilon)])$ and $\mu'_5 = \{ x = \mu'_6(\var{xs}), \var{ys} = \mu'_6(\var{ys})\}$.
Again, in the backward evaluation of $\var{appendBbody}$, we know from the trace $\var{tr}_5$ that the second branch (cons case) must be chosen, and from the original environment $\{ \var{xs} = [2,3], \dots \}$ that the branch is the original one. Thus, the last rule used for the evaluation must be Tp-BCase1.

Thus, to make the above traced backward evaluation hold, it suffices (and needs) that the following conditions hold (again, we shall ignore irrelevant premises of Tp-BCase1).

\begin{gather*}
\EvalRelU{(\var{not} \circ \var{null}) \A [2] }{ \con{True} } \\
\EvalRelBT{ \{a = 2, x = [3], \var{ys} = [4,5], \dots\} }{ a \bxop{:} \var{appendB} \A x \A \var{ys} }{ [2] }{[\epsilon, \var{tr}_6]}{ \mu'_7 \uplus_{\{\var{ys}, \dots\}, \{a,x\}} \mu'_8 } \tag{\ensuremath{\ast\ast}}\label{prop:put2}\\
\EvalRelBT{ \{ \var{xs} = [2,3], \dots \} }{ \var{xs} }{ \sem{a : x}^{-1} (\mu_8' \triangleleft \{ a = 2, x = [3] \}) }{\epsilon}{ \mu'_9 }  \\
\mu'_6 = \mu'_7 \lub \mu'_9
\end{gather*}

The first condition clearly holds, and the third condition can be solved by Tp-Var with
$\mu'_9 = \{ \var{xs} = \sem{a : x}^{-1} (\mu_8' \triangleleft \{ a = 2, x = [3] \})$.
The second condition (<ref>) is further reduced to conditions:

\begin{gather*}
\EvalRelBT{ \{a = 2, \dots\} }{ a  }{ 2 }{\epsilon}{ \mu'_{10} } \\
\EvalRelBT{\{\var{xs} = [3], \var{ys} = [4,5], \dots \}}{\var{appendBbody}}{[\,]}{\var{tr}_6}{\mu'_{11}}\\
\mu'_7 \uplus_{\{\var{ys}, \dots\}, \{a,x\}} \mu'_8 = \mu'_{10} \lub \{ \var{x} = \mu'_{11}(\var{xs}), \var{ys} = \mu'_{11}(\var{ys}) \}\text{.}
\end{gather*}

Clearly, by Tp-Var, the first condition holds with $\mu'_{10} = \{ a = 2 \}$.
Thus, let's focus on the second condition.
Unlike the previous cases, the trace $\var{tr}_6 = \mathrm{Br}(\epsilon,0,\epsilon)$ says that the evaluation must use the first branch (nil case),
which is different from the original branch (taken under the environment $\{ \var{xs} = [3], \dots \}$).
Thus, the last rule used in the evaluation
\(
\EvalRelBT{\{\var{xs} = [3], \var{ys} = [4,5], \dots \}}{\var{appendBbody}}{[\,]}{\var{tr}_6}{\mu'_{11}}
\)
must be Tp-BCase2, meaning that branch switching happened. Since we have

\[
\EvalRelU{ (\lambda \dontcare. \lambda \dontcare.\, [\,]) \A [3] \A [\,] }{ [\,] }
\]

we then check other premises of the rule instance (again, we shall ignore the irrelevant ones):

\begin{gather*}
\EvalRelU{(\var{not} \circ \var{null}) \A [\,]}{\con{False}} \\
\EvalRelU{(\var{const} \A \con{True}) \A [\,]}{\con{True}} \\
\EvalRelBT{ \{ \var{ys} = [4,5], \dots \} }{ \var{ys} }{ [\,] }{ \epsilon }{ \mu'_{12} \uplus_{\{ \var{ys}, \dots\}, \emptyset} \emptyset} \\
\EvalRelBT{ \{ \var{xs} = [3], \dots \}  }{ \var{xs} }{ \sem{ [\,] }^{-1}(\emptyset \triangleleft \emptyset) }{ \epsilon }{ \mu'_{13} }\\
\mu'_{11} = \mu'_{12} \lub \mu'_{13}\text{.}
\end{gather*}

The first two clearly hold, and by Tp-Var, the third and forth ones hold with  $\mu'_{12} = \{ \var{ys} = [\,] \}$ and $\mu'_{13} = \{ \var{xs} = [\,] \}$.
Thus, we have $\mu'_{11} = \{ \var{xs} = [\,], \var{ys} = [\,] \}$ to satisfy the fifth condition.
Then, we can solve the constraints on environments obtained so far as:
$\mu'_8 = \{ a = 2, x = [\,] \}$,
$\mu'_7 = \{ \var{ys} = [\,] \}$,
$\mu'_9 = \{ \var{xs} = [2] \}$,
$\mu'_6 = \{ \var{xs} = [2], \var{ys} = [\,] \}$,
$\mu'_5 = \{ x = [2], \var{ys} = [\,] \}$,
$\mu'_1 = \{ \var{ys} = [\,] \}$,
$\mu'_2 = \{ a = 6, x = [2] \}$, and
$\mu'_3 = \{ \var{xs} = [6,2] \}$. Now, we are ready to check $\mu' = \{ \var{xs} = [6,2], \var{ys} = [\,] \} = \mu'_1 \lub \mu'_3$ to conclude (<ref>).

§ APPENDIX

§.§ Full Definition of Typing Relation

The complete definition of (our fragment of) HOBiT's typing relation is given in Fig. <ref>.
The definition assumes constructors have simple types $\con{C} : A_1 \to \dots \to A_n \to A$, which
may be instantiation results of their (rank-1) polymorphic types (such as list constructors $(:)$ and $[\,]$).

$\Gamma; \Delta \vdash e : A$

\begin{gather*}
\infer
{ \Gamma; \Delta \vdash x : A  }
{ \Gamma(x) = A }
\quad
\infer
{ \Gamma; \Delta \vdash x : \BX{\tau}}
{ \Delta(x) = \tau }
\quad
\infer
{ \Gamma; \Delta \vdash \lambda x.e : A \to B }
{ \Gamma, x:A; \Delta \vdash e : B }
\quad
\infer
{ \Gamma; \Delta \vdash e_1 \A e_2 : B }
{ \Gamma; \Delta \vdash e_1 : A \to B
\quad
\Gamma; \Delta \vdash e_2 : A }
\\
\infer
{\Gamma; \Delta \vdash \con{C} \A \V{e}: A }
{ \{ \Gamma; \Delta \vdash e : A_i \}_i \quad \con{C} : A_1 \to \dots \to A_n \to A   }
% \quad
% \infer
% {\Gamma; \Delta \vdash \con{False} : \con{Bool}}
% {}
% \quad
% \infer
% {\Gamma; \Delta \vdash [\,] : [A]}
% {}
% \quad
% \infer
% { \Gamma; \Delta \vdash (e_1 : e_2) : [A] }
% { \Gamma; \Delta \vdash e_1 : A
% \quad
% \Gamma; \Delta \vdash e_2 : [A]
% }
\quad
\infer
{ \Gamma; \Delta \vdash \CASE~e_0~\OF~\{ p_i \to e_i \}_i : B }
{ \Gamma; \Delta \vdash e_0  : A
\quad
\{ \Gamma_i \vdash p_i : A \quad \Gamma, \Gamma_i ; \Delta \vdash e_i : B \}_i
\\
\infer
{ \Gamma ; \Delta \vdash \LIFTU{e} : \BX{\tau} }
{ \Gamma ; \Delta \vdash e : \tau }
\quad
\infer
{ \Gamma ; \Delta \vdash \bxcon{C} \A \V{e}: \BX{\tau} }
{ \{ \Gamma; \Delta \vdash e_i : \BX{\tau_i} \}_i
\quad
\con{C} : \tau_1 \to \dots \to \tau_n \to \tau
% \infer
% {\Gamma; \Delta \vdash \bx{\con{True}} : \BX{\con{Bool}}}
% {}
% \quad
% \infer
% {\Gamma; \Delta \vdash \bx{\con{False}} : \BX{\con{Bool}}}
% {}
% \quad
% \infer
% {\Gamma; \Delta \vdash \bx{[\,]} : \BX{[\tau]}}
% {}
% \quad
% \infer
% { \Gamma; \Delta \vdash (e_1 \mathbin{\bx{:}} e_2) : \BX{[\tau]} }
% { \Gamma; \Delta \vdash e_1 : \BX{\tau}
%   \quad
%   \Gamma; \Delta \vdash e_2 : \BX{[\tau]}
% }
\\
\infer
{ \Gamma; \Delta \vdash \BCASE~e_0~\BOF~\{ {{p_i}} \to e_i~\BWITH~e'_i~\BBY~e''_i \}_i : \BX{\sigma} }
{ \Gamma; \Delta \vdash e_0 : \BX{\tau}
\quad
\{ \Delta_i \vdash p_i : A \quad \Gamma ; \Delta, \Delta_i \vdash e_i : B \quad \Gamma; \Delta \vdash e'_i : \sigma \to \con{Bool} \quad \Gamma; \Delta \vdash e''_i : \tau \to \sigma \to \tau  \}_i
\end{gather*}

$\Gamma \vdash p : A$

\begin{gather*}
\infer
{ x: A \vdash x : A }
\quad
\infer
{\Gamma_1,\dots,\Gamma_n \vdash \con{C} \A \V{p} : A  }
{ \{ \Gamma_i \vdash p_i : A_i \}
\quad
\con{C} : A_1 \to \dots \to A_n \to A
% \infer
% { \emptyset \vdash \con{True} : \con{Bool} }
% {}
% \quad
% \infer
% { \emptyset \vdash \con{False} : \con{Bool} }
% {}
% \quad
% \infer
% { \emptyset \vdash [\,] : [A] }
% { }
% \quad
% \infer
% { \Gamma_1,\Gamma_2 : (e_1 : e_2) : [A] }
% { \Gamma_1 \vdash e_1 : A
% \quad
% \Gamma_2 \vdash e_2 : [A] }
\end{gather*}

$\Gamma \vdash P$

\begin{gather*}
\infer
{ \Gamma \vdash f_1 = e_1; \dots ; f_n = e_n  }
{ \{ \Gamma ; \emptyset \vdash e_i : \Gamma(f_i) \}_{i} }
\end{gather*}

Typing rules: $\Delta \vdash p : \sigma$ is defined similarly to $\Gamma \vdash p : A$ but asserts that the resulting environment is actually an bidirectional one and every type that occurs in the derivation is a $\sigma$-type.

§.§ Full Definition of Sketch Generation Rules

Figure <ref> provides the sketch generation rules used in Section <ref>.

For simplicity of presentation, in Section <ref> we did not explicitly capture the type of the code to be generated in the specialized holes as it can be recovered from the sketch and typing environment $\Gamma$. However, here we make it explicit by augmenting
both the exit condition hole and the reconciliation hole with
the typing environment $\Gamma$ and the type of the code to be
synthesized: $\EHole{\Gamma}{\sigma \to \con{Bool}}{e}$ and
$\RHole{\Gamma}{\sigma_0 \to \sigma \to \sigma_0}{p}{e}$.

\begin{gather*}
\ninfer
{ \GenTmp{\Gamma'}{\Delta'}{\BX{\tau}}{\Gamma}{e}{\tau}{\LIFTU{e'}} }
{ \GenTmp{\Gamma'}{\Delta'}{\tau}{\Gamma}{e}{\tau}{e'} }
\quad
\ninfer
{ \GenTmp{\Gamma'}{\Delta'}{A'}{\Gamma}{x}{A}{x}}
{ x:A\in\Gamma\quad x:A'\in\Gamma' }
\quad
\ninfer
{ \GenTmp{\Gamma'}{\Delta'}{\BX{\sigma}}{\Gamma}{x}{\sigma}{x} }
{ x:\sigma\in\Gamma\quad x:\sigma\in\Delta' }
\\
\ninfer
{ \GenTmp{\Gamma'}{\Delta'}{(A_1'\to A_2')}{\Gamma}{\lambda x.e}{A_1\to A_2}{\lambda x.e'} }
{ \GenTmp{(\Gamma',x:A_1')}{\Delta'}{A_2'}{(\Gamma,x:A_1)}{e}{A_2}{e'} }
\\
\ninfer
{ \GenTmp{\Gamma'}{\Delta'}{A'}{\Gamma}{e_1 \A e_2}{A}{e_1' \A e_2'} }
{ \begin{tarray}{c}
\GenTmp{\Gamma'}{\Delta'}{(A_2'\to A')}{\Gamma}{e_1}{(A_2\to A)}{e_1'} \quad
A_2 \leadsto B_2 \quad
\GenTmp{\Gamma'}{\Delta'}{B_2}{\Gamma}{e_2}{A_2}{e_2'}
\end{tarray}
\\
\ninfer
\GenTmp{\Gamma'}{\Delta'}{A}{\Gamma}{\con{C} \A \V{e}}{A}{\con{C} \A \V{e'}}
\con{C} : A_1 \to \dots \to A_n \to A \quad
\{ \GenTmp{\Gamma'}{\Delta'}{A_i}{\Gamma}{e_i}{A_i}{e'_i}  \}_i
\\
\ninfer
\GenTmp{\Gamma'}{\Delta'}{\BX{\tau}}{\Gamma}{\con{C} \A \V{e}}{\tau}{\bxcon{C} \A \V{e'}}
\con{C} : \tau_1 \to \dots \to \tau_n \to \tau \quad
\{ \GenTmp{\Gamma'}{\Delta'}{\BX{\tau_i}}{\Gamma}{e_i}{\tau_i}{e'_i}  \}_i
\\
\ninfer
{ \GenTmp{\Gamma'}{\Delta'}{A'}{\Gamma}{\CASE~e_0~\OF~\{ p_i \to e_i \}_i}{A}{\CASE~e_0'~\OF~\{ p_i \to e_i' \}_i} }
{ \begin{tarray}{c}
\GenTmp{\Gamma'}{\Delta'}{A_0'}{\Gamma}{e_0}{A_0}{e_0'} \quad
A_0 \leadsto A_0' \\
\{ \Gamma_i\vdash p_i: A_0 \quad
\Gamma'_i \vdash p_i : A_0' \quad
\GenTmp{(\Gamma',\Gamma_i')}{\Delta'}{A'}{(\Gamma,\Gamma_i)}{e_i}{A}{e_i'}  \}_i
\end{tarray} }
\\
\ninfer
{ \GenTmp{\Gamma'}{\Delta'}{\BX{\sigma}}{\Gamma}{\CASE~e_0~\OF~\{ p_i \to e_i \}_i}{\sigma}{\BCASE~e_0'~\BOF
\left\{\begin{tarray}{l}
\displaystyle \bx{{p_i}} \to e_i'                                         \\
\displaystyle \BWITH~\EHole{\Gamma'}{\sigma \to \con{Bool}}{e_i'} \\
\displaystyle \BBY~\RHole{\Gamma'}{\sigma_0 \to \sigma \to \sigma_0}{p_i}{e_i}
\end{tarray}\right\}_i}}
{ \begin{tarray}{c}
\GenTmp{\Gamma'}{\Delta'}{\BX{\sigma_0}}{\Gamma}{e_0}{\sigma_0}{e_0'} \\
\{\Gamma_i\vdash p_i: \sigma_0 \quad
\Delta'_i \vdash p_i : \sigma_0 \quad
\GenTmp{\Gamma'}{(\Delta',\Delta_i')}{\BX{\sigma}}{(\Gamma,\Gamma_i)}{e_i}{\sigma}{e_i'}
\end{tarray} }
\end{gather*}

Sketch generation rules for expressions

Discussion on -polymorphism

supports $\LET$-polymorphism as illustrated by some $\GET$ programs used in the experiments (Section <ref>), such as $\var{append} :: [a] \to [a] \to [a]$ and $\var{reverse} :: [a] \to [a]$ that have polymorphic types.
However, for simplicity, we assumed simple types in our formal development (, Fig. <ref> and <ref>).

The handling of bidirectional programs with (rank 1) polymorphic types is mostly straightforward. For example, for the sketch generation in Fig. <ref>,
we can leverage the fact that in the standard typing system for $\LET$ polymorphism <cit.>, expressions can only have monomorphic types.
As a consequence, we can say $A$ and $A$' in $\GenTmp{\Gamma'}{\Delta'}{A'}{\Gamma}{e}{A}{e'}$ are always monomorphic.
Also, these types $A$ and $A$' are fully determined in advance of the generation,
because $A$ comes from the typing derivation of the original $\GET$ program and $A'$ is obtained form $A$ by inserting $\BX{}$. The types $A$ and $A$' may contain
type variables but they are rigid (, not subject to unification).
Note that we can access to the typing derivation of the original $\GET$ program as well as the code itself.

Though it is still straightforward, a slightly more careful discussion is needed for the type-directed generation of terms to fill shape-restricted holes (Section <ref>), where types being used for type-directed generation may not be immediately clear.
In an extreme case, for example, if the component functions contains $\var{const} :: a \to b \to a$, we have no immediate information of the type
to generate its second argument as it cannot be determined by instantiation of $a$.
This suggests that we may need to consider explicit handing of type variables and unification
in the term generation, which complicates the system.

Fortunately though, our back-end system for (lazy) nondeterministic generation is powerful enough to address the issue without introducing any additional complication;
in the system, a logic (, unifiable) variable (, (non-rigid) type variable) can be expressed by
nondeterministic generation of all the things (, monomorphic types) to substitute for it,
and by the $\var{share}$ operator <cit.>.

§.§ Full Definition of Filtering based on Branch Traces

§.§.§ Formal Semantics of HOBiT

To understand definition of filtering based on branch traces, one needs to know the formal semantics of HOBiT.
The semantics of HOBiT is defined so that a term-in-context $\emptyset; \Delta \vdash e : \BX{\sigma}$ defines a bidirectional transformation between $\Delta$ and $\sigma$.
However, it is not clear how to interpret function abstractions and applications to achieve this goal.
Thus, HOBiT adopts the staged semantics; it first evaluates $\lambda$s away to obtain a first-order residual expression $E$ from $e$, and
then interprets $E$ as a bidirectional transformation between $\Delta$ and $\sigma$.
Specifically, we use three evaluation relations:
$\EvalRelU{e}{v}$ is for unidirectional evaluation to obtain residual expressions, and
$\EvalRelF{\mu}{E}{u}$ and $\EvalRelB{\mu}{E}{u}{\mu'}$ for bidirectional evaluation of residual expressions.

Values $v$, residual expressions $E$ and first-order values $u$ are defined as follows.

\[
\begin{tarray}{lcll}
v &::=& \con{True} \mid \con{False} \mid [\,] \mid v_1 : v_2 \mid \lambda x.e \mid E \\
E &::=& x \mid  \bx{\con{True}} \mid \bx{\con{False}} \mid \bx{[\,]} \mid E_1 \mathbin{\bx{:}} E_2 \mid \CASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~v'_i~\BY~v''_i \}_i \mid \LIFTU{u} \\
u &::=& \con{True} \mid \con{False} \mid [\,] \mid u_1 : u_2
\end{tarray}
\]

Intuitively, $v$, $E$, and $u$ represent evaluation results of $A$-, $\BX{\tau}$-, and $\tau$-typed expressions, respectively.
Note that $e$/$e_i$ appears under $\lambda$ or $\CASE$, meaning that their evaluates are delayed.

\begin{gather*}
\infer
\quad
\infer
{(f = e) \in P \quad \EvalRelU{e}{v}}
\quad
\infer
{\EvalRelU{e_1 \A e_2}{v}}
{\EvalRelU{e_1}{\lambda x.e} \quad
\EvalRelU{e_2}{v_2} \quad
\EvalRelU{e[v_2/x]}{v}
\quad
\infer
{\EvalRelU{\lambda x.e}{\lambda x.e}}
\\
\infer
\EvalRelU{\CASE~e_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~e'_i~\BY~e''_i \}_i}{\CASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~v'_i~\BY~v''_i \}_i}
\EvalRelU{e_0}{E_0} \quad
\{ \EvalRelU{e'_i}{v'_i} \quad \EvalRelU{e''_i}{v''_i} \}_i
% \quad
% \text{$\fv(p_i)$: fresh}
\end{gather*}

Unidirectional Evaluation Rules (Excerpt)

Unidirectional evaluation The rules for the unidirectional evaluation relation is rather standard, as excerpted in Fig. <ref>.
The bidirectional constructs (, bidirectional constructors and bidirectional $\CASE$) are frozen, , treated as
ordinary constructors in this evaluation.

Bidirectional ($\GET$ and $\PUT$) evaluation relations
The $\GET$ and $\PUT$ evaluation relations, $\EvalRelF{\mu}{E}{u}$ and $\EvalRelB{\mu}{E}{u}{\mu'}$,
are defined so that they form a bidirectional transformation.
A caveat here is that the $\PUT$ evaluation relation returns an environment of which domain is $\fv(E)$.

\[
\begin{array}{c@{\quad}c@{\quad}c@{\quad}c}
\displaystyle
\infer
{\EvalRelF{\mu}{x}{\mu(x)} }
%  &
% \displaystyle
% \infer
% { \EvalRelF{\mu}{\bx{c}}{c} }
% { c = \con{True}, \con{False}, [\,] }
\displaystyle
\infer
{ \EvalRelF{\mu}{\bxcon{C} \A \V{e}}{ \con{C} \A \V{u} } }
{ \{ \EvalRelF{\mu}{e_i}{u_i} \}_i }
\displaystyle
\infer
{ \EvalRelF{\mu}{ \LIFTU{u} }{ u } }
{ }
\\[10pt]
\displaystyle
\infer
{\EvalRelB{\mu}{x}{u}{ \{x = u\} } }
%  &
% \displaystyle
% \infer
% { \EvalRelB{\mu}{\bx{c}}{c}{ \emptyset }  }
% { c = \con{True}, \con{False}, [\,] }
\displaystyle
\infer
{ \EvalRelB{\mu}{ \bxcon{C} \A \V{e} }{ \con{C} \A \V{u} }{\textstyle \bigcurlyvee \mu'_i} }
{ \{\EvalRelB{\mu}{e_i}{u_i}{\mu'_i}\}_i }
\displaystyle
\infer
{ \EvalRelB{\mu}{ \LIFTU{u} }{ u }{\emptyset} }
{  }
\end{array}
\]

$\GET$ and $\PUT$ Evaluation Rules (except $\CASE$)

Most $\GET$ and $\PUT$ evaluation rules are straightforward except $\CASE$ (Fig. <ref>).
In the definition, we use the merging operator $\lub$ defined as: $\mu_1 \lub \mu_2 = \mu_1 \cup \mu_2$ if
there is no $x$ such that $\mu(x) \ne \mu'(x)$.

The most interesting rules are those for $\CASE$. In the $\GET$ direction, the evaluation rule is similar to the ordinary one
except that it involves runtime check of exit conditions.

\[
\infer
{ \EvalRelF{\mu}{\CASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~v'_i~\BY~v''_i \} }{ u } }
\EvalRelF{\mu}{E_0}{u_0} \quad
\sem{p_i}\A u_0 = \mu_i \quad
\EvalRelU{e_i}{E_i} \quad
\EvalRelF{\mu \uplus \mu_i}{E_i}{u} \quad
\EvalRelU{v'_i \A u}{\con{True}}
\]

Here, we write $\sem{p}$ for the semantics of pattern matching by $p$: , $\sem{p} \A u$ is a partial function that returns a binding $\mu$
with $\dom(\mu) = \fv(p)$ and $u = p\mu$ if exists (and fails otherwise), where we identity an environment $\mu$ and a substitution.
For this case (even after extension with guards), $\sem{p}$ is injective and thus has a left inverse $\sem{p}^{-1}$, which will be used by the $\PUT$ evaluation of $\CASE$.
The rule implicitly assumes that $\dom(\mu_i)$ (, $\fv(p_i)$) and $\dom(\mu)$ are disjoint;
we assume appropriate $\alpha$-renaming that is consistent in $\GET$ and $\PUT$ to fulfill the condition.
Reconciliation functions are not used at all in the $\GET$ direction.

There are two $\PUT$ evaluation rules for $\CASE$: one is for when there is no branch switching and the other is for when branch switching happens.
We first explain the non-branch-switching one.

\[
\infer
{ \EvalRelB{\mu}{\CASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~v'_i~\BY~v''_i \} }{ u }{ \mu'_0 \lub \mu' } }
\begin{array}{c}
\EvalRelF{\mu}{E_0}{u_0} \quad
\sem{p_i}\A u_0 = \mu_i \quad
\EvalRelU{v'_i \A u}{\con{True}} \\
\EvalRelU{e_i}{E_i} \quad
\EvalRelB{\mu \uplus \mu_i}{E_i}{u}{\mu' \uplus_{\dom(\mu),\dom(\mu_i)} \mu'_i} \quad
\sem{p_i}^{-1} \A (\mu'_i \triangleleft \mu_i) = u_0' \quad
\EvalRelB{\mu}{E_0}{u'_0}{\mu'_0}
\end{array}
\]

Intuitively, the rule says that we use the original branch if its associated exit condition $v'_i$ becomes $\con{True}$ for an updated value $u$.
In this step, we need to separate the backward evaluation result of $E_i$ into two: $\mu'$ for free variables in $E_i$ and $\mu'_i$ for variables introduced by $p_i$.
To express the separation, this rule uses $\mu_1 \uplus_{X,Y} \mu_2$ which behaves similarly to $\mu_1 \uplus \mu_2$, while also ensuring that $\dom(\mu_1) \subseteq X$ and $\dom(\mu_2) \subseteq Y$.
A caveat here is that some $p_i$ variables may not occur in $E_i$, and for such a case $\dom(\mu'_i)$ is strictly smaller than $\fv(p_i)$ ($= \dom(\mu_i)$);
, we may not be ready to apply $\sem{p_i}^{-1}$ that assumes environments with the domain $\fv(p_i)$.
Thus, to apply $\sem{p_i}^{-1}$, the rule uses the operator $\triangleleft$ (read “defaulting by”) defined by:

\[
(\mu \triangleleft \mu')(x) = \begin{cases}
\mu(x)  & \text{if}~x \in \dom(\mu)                      \\
\mu'(x) & \text{if}~x \in \dom(\mu') \setminus \dom(\mu)
\end{cases}
\]

Once the rule applies $\sem{p_i}^{-1}$ to compute an updated value $u'_0$ of $E_0$, it performs the backward evaluation of $E_0$ to obtain $\mu'_0$ and then results in $\mu'_0 \lub \mu'$.
Again, reconciliation functions have no use in this case.

The branch-switching $\PUT$ rule handles the case where the original exit condition becomes $\con{False}$ for an updated value $u$.

\[
\infer
{ \EvalRelB{\mu}{\CASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~v'_i~\BY~v''_i \} }{ u }{ \mu'_0 \lub \mu' } }
\begin{array}{c}
\EvalRelF{\mu}{E_0}{u_0} \quad
\sem{p_i}\A u_0 = \mu_i \quad
\EvalRelU{v'_i \A u}{\con{False}} \quad
\EvalRelU{v'_j \A u}{\con{True}} \quad
\{ \EvalRelU{v'_k \A u}{\con{False}} \}_{k < j}
\\
\EvalRelU{v''_j \A u_0 \A u}{u_0^\mathrm{rec}} \quad
\sem{p_j} \A u_0^\mathrm{rec} = \mu_j
\\
\EvalRelU{e_j}{E_j} \quad
\EvalRelB{\mu \uplus \mu_j}{E_j}{u}{\mu' \uplus_{\dom(\mu),\dom(\mu_j)} \mu'_j} \quad
\sem{p_j}^{-1} \A (\mu'_j \triangleleft \mu_j) = u_0' \quad
\EvalRelB{\mu}{E_0}{u'_0}{\mu'_0}
\end{array}
\]

Then, the rule chooses the branch $j$ of which exit condition becomes $\con{True}$ first (, the first match principle).
We now want to perform the backward evaluation of $E_j$, but this is not immediately possible as we do not know the original environment due to $p_j$.
Pattern-matching with $u_0$ is a non solution as it matches $p_i$ and not likely to match $p_j$.
Thus, we use the associated reconciliation function $v''_j$ to construct a reconciled result $u_0^\mathrm{rec}$ to be matched with $p_j$.
The rest of the behavior is the same as the non-branch switching case.

Here, we provide details on the filtering based on branch traces, corresponding to Section <ref>.

A trace is a tree that preserves information about which branches of $\BCASE$ were chosen during the $\GET$ or $\PUT$ evaluation.
The syntax of such a trace is as follows:

\[\revised{\mathit{tr}  ::= \epsilon \mid \mathrm{Br}(\mathit{tr}_0,j,\mathit{tr}_1) \mid [\mathit{tr}_1,\ldots,\mathit{tr}_n]}
\]

Here, $\mathrm{Br}(\mathit{tr}_0,j,\mathit{tr}_1)$ is a trace for
$\BCASE~E_0~\BOF~\{ p_i \rightarrow e_i~\WITH~v_i'~\BY~v_i''\}_i$, where $\mathit{tr}_0$ is the trace for $E_0$,
$j$ stands for the $j$-th branch that was chosen, and $\mathit{tr}_1$ is the trace for $E_j$.
The traces $\mathit{tr}_1,\ldots,\mathit{tr}_n$ in
$[\mathit{tr}_1,\ldots,\mathit{tr}_n]$ correspond to the arguments of a constructor application $\bxcon{C} \A e_1 \A ,\ldots, \A e_n$. We abbreviate $[\mathit{tr}_1,\ldots,\mathit{tr}_n]$ to $\V{\mathit{tr}}$ when $n$ is obvious.

Primer on HOBiT's formal semantics
To understand the definition of filtering based on branch traces, one needs to know the formal semantics of HOBiT.
The semantics of HOBiT is defined so that a term-in-context $\emptyset; \Delta \vdash e : \BX{\sigma}$ defines a bidirectional transformation between $\Delta$ and $\sigma$.
However, it is not clear how to interpret function abstractions and applications to achieve this goal.
Thus, HOBiT adopts the staged semantics; it first evaluates $\lambda$s away to obtain a first-order residual expression $E$ from $e$, and
then interprets $E$ as a bidirectional transformation between $\Delta$ and $\sigma$.
Specifically, we use three evaluation relations:
$\EvalRelU{e}{v}$ is for unidirectional evaluation to obtain residual expressions, and
$\EvalRelF{\mu}{E}{u}$ and $\EvalRelB{\mu}{E}{u}{\mu'}$ for bidirectional evaluation of residual expressions.

Values $v$, residual expressions $E$ and first-order values $u$ are defined as follows.

\[
\begin{tarray}{lcll}
v &::=& \con{True} \mid \con{False} \mid [\,] \mid v_1 : v_2 \mid \lambda x.e \mid E \\
E &::=& x \mid  \bx{\con{True}} \mid \bx{\con{False}} \mid \bx{[\,]} \mid E_1 \mathbin{\bx{:}} E_2 \mid \CASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~v'_i~\BY~v''_i \}_i \mid \LIFTU{u} \\
u &::=& \con{True} \mid \con{False} \mid [\,] \mid u_1 : u_2
\end{tarray}
\]

Intuitively, $v$, $E$, and $u$ represent evaluation results of $A$-, $\BX{\tau}$-, and $\tau$-typed expressions, respectively.

For more details on HOBiT, please see HOBiT's original paper <cit.>.

's evaluation rules with traces
The rules for the unidirectional evaluation relation are rather standard, as excerpted in Fig. <ref>.
The bidirectional constructs (, bidirectional constructors and bidirectional $\CASE$) are frozen, , treated as
ordinary constructors in this evaluation.

For filtering based on trace branches we make use of the evaluation relations $\EvalRelFT{\mu}{E}{u}{\mathit{tr}}$ and $\EvalRelBT{\mu}{E}{u}{\mathit{tr}}{\mu'}$,
defined by the rules in Fig. <ref>.
Intuitively, $\EvalRelFT{\mu}{E}{v}{\mathit{tr}}$ means that a program $E$ is reduced to the original view $v$ under the the original source environment $\mu$ through a trace $\mathit{tr}$.

Accordingly, $\EvalRelBT{\mu}{E}{v}{\mathit{tr}}{\mu'}$ means that a program $E$ is evaluated according to its $\PUT$ behavior such that the
updated source $\mu'$ is obtained from the the original source $\mu$ and the updated view $v$ through a trace $\mathit{tr}$.

These traced evaluation relations only differ from the original $\GET$ and $\PUT$ evaluation relations <cit.> in reference to traces.
Thus, we omit the definitions of the original, untraced evaluation relations $\EvalRelF{\mu}{E}{u}$ and $\EvalRelB{\mu}{E}{u}{\mu'}$, whereas
they appear in Fig. <ref>.

In the evaluation rules, we write $\sem{p}$ for the semantics of pattern matching by $p$: , $\sem{p} \A u$ is a partial function that returns a binding $\mu$
with $\dom(\mu) = \fv(p)$ and $u = p\mu$ if such $\mu$ exists (and fails otherwise).
In HOBiT, $\sem{p}$ is injective and thus has a left inverse $\sem{p}^{-1}$.
The rules for $\BCASE$ (, Tg-BCase, Tp-BCase1, and Tp-BCase2) implicitly assume that $\dom(\mu_i)$ (, $\fv(p_i)$) and $\dom(\mu)$ are disjoint;
we assume appropriate $\alpha$-renaming that is consistent in $\GET$ and $\PUT$ to fulfill the condition.
To separate environments, the evaluation rules use $\mu_1 \uplus_{X,Y} \mu_2$ which behaves similarly to $\mu_1 \uplus \mu_2$, while also ensuring $\dom(\mu_1) \subseteq X$ and $\dom(\mu_2) \subseteq Y$.
The operator $\triangleleft$ is defined by:

\[
(\mu' \triangleleft \mu)(x) = \begin{cases}
\mu'(x)  & \text{if}~x \in \dom(\mu')                      \\
\mu(x) & \text{if}~x \in \dom(\mu) \setminus \dom(\mu')
\end{cases}
\]

The operator $\lub$ is defined as: $\mu_1 \lub \mu_2 = \mu_1 \cup \mu_2$ if $\mu_1(x) = \mu_2(x)$ for all $x \in \dom(\mu_1) \cap \dom(\mu_2)$,
and otherwise $\mu_1 \lub \mu_2$ is undefined.

\begin{gather*}
\infer
\quad
\infer
{(f = e) \in P \quad \EvalRelU{e}{v}}
\quad
\infer
{\EvalRelU{e_1 \A e_2}{v}}
{\EvalRelU{e_1}{\lambda x.e} \quad
\EvalRelU{e_2}{v_2} \quad
\EvalRelU{e[v_2/x]}{v}
\quad
\infer
{\EvalRelU{\lambda x.e}{\lambda x.e}}
\\
\infer
\EvalRelU{\CASE~e_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~e'_i~\BY~e''_i \}_i}{\CASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~v'_i~\BY~v''_i \}_i}
\EvalRelU{e_0}{E_0} \quad
\{ \EvalRelU{e'_i}{v'_i} \quad \EvalRelU{e''_i}{v''_i} \}_i
% \quad
% \text{$\fv(p_i)$: fresh}
\end{gather*}

Unidirectional evaluation rules (excerpt)

\begin{gather*}
\begin{array}{c@{\quad}c@{\quad}c@{\quad}c}
\displaystyle
\ninfer{Tg-Var}
{\EvalRelFT{\mu}{x}{\mu(x)}{\TrNil} }
%  &
% \displaystyle
% \infer
% { \EvalRelFT{\mu}{\bx{c}}{c}{\TrNil} }
% { c = \con{True}, \con{False}, [\,] }
\displaystyle
\ninfer{Tg-BCon}
{ \EvalRelFT{\mu}{\bxcon{C} \A \V{e}}{\con{C} \A \V{u}}{\V{\mathit{tr}}} }
{ \{\EvalRelFT{\mu}{e_i}{u_i}{\mathit{tr}_i} \}_i}
\displaystyle
\ninfer{Tg-!}
{ \EvalRelFT{\mu}{ \LIFTU{u} }{ u }{\TrNil} }
{ }
\\[10pt]
\displaystyle
\ninfer{Tp-Var}
{\EvalRelBT{\mu}{x}{u}{\TrNil}{ \{x = u\} } }
%  &
% \displaystyle
% \infer
% { \EvalRelBT{\mu}{\bx{c}}{c}{\TrNil}{ \emptyset }  }
% { c = \con{True}, \con{False}, [\,] }
\displaystyle
\ninfer{Tp-BCon}
{ \EvalRelBT{\mu}{ \bxcon{C} \A \V{e} }{ \con{C} \A \V{u} }{\V{\mathit{tr}}}{\bigcurlyvee \mu'_i } }
{ \{\EvalRelBT{\mu}{e_i}{u_i}{\mathit{tr}_i}{\mu'_i}\}_i }
\displaystyle
\ninfer{Tp-!}
{ \EvalRelBT{\mu}{ \LIFTU{u} }{ u }{\TrNil}{\emptyset} }
{  } \\[10pt]
\end{array}\\
\ninfer{Tg-BCase}
{ \EvalRelFT{\mu}{\BCASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\BWITH~v'_i~\BBY~v''_i \} }{ u }{ \TrBranch{\mathit{tr}_0}{i}{\mathit{tr}_i} } }
\EvalRelFT{\mu}{E_0}{u_0}{\mathit{tr}_0} \quad
\sem{p_i}\A u_0 = \mu_i \quad
\EvalRelU{e_i}{E_i} \quad
\EvalRelFT{\mu \uplus \mu_i}{E_i}{u}{\mathit{tr}_i} \quad
\EvalRelU{v'_i \A u}{\con{True}}
\ninfer{Tp-BCase1}
{ \EvalRelBT{\mu}{\BCASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\BWITH~v'_i~\BBY~v''_i \} }{ u }{ \TrBranch{\mathit{tr}_0}{i}{\mathit{tr}_i} }{ \mu'_0 \lub \mu' } }
\begin{array}{c}
\EvalRelF{\mu}{E_0}{u_0} \quad
\sem{p_i}\A u_0 = \mu_i \quad
\EvalRelU{v'_i \A u}{\con{True}} \\
\EvalRelU{e_i}{E_i} \quad
\EvalRelBT{\mu \uplus \mu_i}{E_i}{u}{\mathit{tr}_i}{\mu' \uplus_{\dom(\mu),\dom(\mu_i)} \mu'_i} \quad
\sem{p_i}^{-1} \A (\mu'_i \triangleleft \mu_i) = u_0' \quad
\EvalRelBT{\mu}{E_0}{u'_0}{\mathit{tr}_0}{\mu'_0}
\end{array}
\ninfer{Tp-BCase2}
{ \EvalRelBT{\mu}{\BCASE~E_0~\OF~\{ \bx{{p_i}} \to e_i ~\BWITH~v'_i~\BBY~v''_i \} }{ u }{ \TrBranch{\mathit{tr}_0}{j}{\mathit{tr}_i} }{ \mu'_0 \lub \mu' } }
\begin{array}{c}
\EvalRelF{\mu}{E_0}{u_0} \quad
\sem{p_i}\A u_0 = \mu_i \quad
\EvalRelU{v'_i \A u}{\con{False}} \quad
\EvalRelU{v'_j \A u}{\con{True}} \quad
\{ \EvalRelU{v'_k \A u}{\con{False}} \}_{k < j}
\\
\EvalRelU{v''_j \A u_0 \A u}{u_0^\mathrm{rec}} \quad
\sem{p_j} \A u_0^\mathrm{rec} = \mu_j
\\
\EvalRelU{e_j}{E_j} \quad
\EvalRelBT{\mu \uplus \mu_j}{E_j}{u}{ \mathit{tr}_i }{\mu' \uplus_{\dom(\mu),\dom(\mu_j)} \mu'_j} \quad
\sem{p_j}^{-1} \A (\mu'_j \triangleleft \mu_j) = u_0' \quad
\EvalRelBT{\mu}{E_0}{u'_0}{ \mathit{tr}_0 }{\mu'_0}
\end{array}
\end{gather*}

$\GET$ and $\PUT$ evaluation rules with traces

For illustration, we use $\var{appendB}$, and assume the following example was given as the backward behavior:

\[
\texttt{:put} \A (\var{uncurryB}~ \var{appendB}) \A ([1,2,3], [4,5]) \A [6,2]  = ([6,2], [\,])
\]

The trace of

\[
\texttt{:get} \A (\var{uncurryB}~ \var{appendB}) \A ([6,2], [\,])  = [6,2]
\]

and the trace of the above $\texttt{:put}$ must coincide.

The trace of this $\texttt{:get}$ (after evaluating $\var{uncurryB}$) is obtained as follows:

\[ \EvalRelFT{\{\var{xs} = [6,2], \var{ys} = [\,]\}}{\var{appendBbody}}{[6,2]}{\mathrm{Br}(\epsilon,1,[\epsilon,\mathrm{Br}(\epsilon,1,[\epsilon,\mathrm{Br}(\epsilon,0,\epsilon)])])}\]

appendBbody =  xs
[ ]      →ys      const True      λ.λ.  [ ]

a : x     →a : appendB x ys      not ∘null      λs.λ.  s

Here, the resulting overall trace is $\mathit{tr} = \mathrm{Br^1}(\epsilon^2,1,[\epsilon^3,\mathrm{Br^4}(\epsilon^5,1,[\epsilon^6,\mathrm{Br^7}(\epsilon^8,0,\epsilon^9)])])$ (for easy identification, we numbered the individual traces). Next, we explain how this is obtained.
The first step of the evaluation of $\GET$ is the case branch.
Since we have $\var{xs} = [6,2]$, the second branch (cons case) is chosen.
Thus, by Tg-BCase, the whole trace $\var{tr}$ has the form of $\mathrm{Br^1}(\var{tr}_2, 1, \var{tr}_3)$,
where $\var{tr}_2$ is the trace of the evaluation of $\var{xs}$, and $\var{tr}_3$ is the trace of the evaluation of $a \bxop{:} \var{appendB} \A x \A \var{ys}$ under $\{a = 6, x = [2],  \var{ys} = [\,], \dots\}$.

By Tg-Var, we have $\var{tr}_2 = \epsilon^2$, and
by Tg-BCon, we have $\var{tr}_3 = [\var{tr}_4, \var{tr}_5]$ for some trace $\var{tr}_4$ and $\var{tr}_5$.
Since $\var{tr}_4$ is the trace of the evaluation of $\var{a}$, we have $\var{tr}_4 = \epsilon^3$ by Tg-Var.
Then, we focus on $\var{tr}_5$, which is the trace of the evaluation of $\var{appendB} \A x \A \var{ys}$ under $\{x = [2], \var{ys} = [\,], \dots\}$.
Thus, we have[If we follow the evaluation rules precisely, we will evaluate $\var{appendBbody}[x/\var{xs}, \var{ys}/\var{ys}]$ with $\alpha$-renaming of $a$ and $x$ bound in $\var{appendBbody}$, which would bring further complication and thus is ignored here.]

\[
\EvalRelFT{\{\var{xs} = [2], \var{ys} = [\,], \dots\}}{\var{appendBbody}}{v_5}{\var{tr}_5}
\]

for some value $v_5$.
The second branch (cons case) is again chosen, and we obtain $\var{tr}_5 = \mathrm{Br^4}(\epsilon^5,1,[\epsilon^6,\mathit{tr}_6])$ for some trace $\mathit{tr}_6$.
Since $\var{tr}_6$ is the trace of the evaluation of $\var{appendB} \A x \A \var{ys}$ under $\{x = [\,], \var{ys} = [\,], \dots\}$, we have

\[
\EvalRelFT{\{\var{xs} = [\,], \var{ys} = [\,], \dots\}}{\var{appendBbody}}{v_6}{\var{tr}_6}
\]

for some value $v_6$.
Since we have $\var{xs} = [\,]$, the first branch (nil case) is chosen. Thus, by Tg-BCon, we have $\var{tr}_6 = \mathrm{Br^7}(\var{tr}_7, 0, \var{tr}_8)$ for some $\var{tr}_7$ and $\var{tr}_8$.
Since $\var{tr}_7$ is the trace of the evaluation of $\var{xs}$, we have $\var{tr}_7 = \epsilon^8$ by Tg-Var.
By Tg-Var, we have $\var{tr}_8 = \epsilon^9$.
As a result, the whole trace of the $\GET$ direction is computed as:

\[\mathit{tr} = \mathrm{Br^1}(\epsilon^2,1,[\epsilon^3,\mathrm{Br^4}(\epsilon^5,1,[\epsilon^6,\mathrm{Br^7}(\epsilon^8,0,\epsilon^9)])])\]

Then, we check if $\texttt{:put} \A (\var{uncurryB}~ \var{appendB}) \A ([1,2,3], [4,5]) \A [6,2] $ goes through the same trace $\mathit{tr}$ as $\GET$.

Essentially, this means that the following relation must hold:

\[
\EvalRelBT{\{\var{xs} = [1,2,3], \var{ys} = [4,5]\}}{\var{appendBbody}}{[6,2]}{\mathrm{Br}(\epsilon,1,[\epsilon,\mathrm{Br}(\epsilon,1,[\epsilon,\mathrm{Br}(\epsilon,0,\epsilon)])])}{\mu'}
\tag{\textdagger}\label{prop:goal}
\]

with $\mu' = \{ \var{xs} = [6,2], \var{ys} = [\,] \}$.
In this evaluation, we also make use of the trace to determine the rule to be applied.
For example, in the backward evaluation of $\var{appendBbody}$ above, we know from the trace that the second branch (cons case) is chosen.
Also, we know from the original environment, which maps $\var{xs}$ to $[1,2,3]$, that branch switching does not happen.
Thus, the last rule used in the evaluation must be Tp-BCase1.

Then, we need to check the following conditions that appear as the premises of the rule (we shall omit the $\GET$ evaluation of scrutinee and the obvious pattern matching as they are not relevant here).

\begin{gather*}
\EvalRelU{(\var{not} \circ \var{null}) \A [6,2]}{\con{True}}\\
\EvalRelBT{ \{a = 1, x = [2,3], \var{ys} = [4,5], \dots\} }{ a \bxop{:} \var{appendB} \A x \A \var{ys} }{ [6,2] }{\var{tr}_3}{ \mu'_1 \uplus_{\{\var{ys}, \dots\}, \{a,x\}} \mu'_2 } \tag{\ensuremath{\ast}}\label{prop:put1}\\
\EvalRelBT{ \{ \var{xs} = [1,2,3], \dots \} }{ \var{xs} }{ \sem{a : x}^{-1} (\mu_2' \triangleleft \{ a = 1, x = [2,3] \}) }{\var{tr}_2}{ \mu'_3 }\\
\mu' = \mu'_1 \lub \mu'_3
%    \EvalRelBT{ \{
\end{gather*}

Here, $\var{tr}_2, \var{tr}_3, \dots$ are the traces that appeared in the $\GET$ evaluation; hence $\var{tr}_2 = \epsilon$ and $\var{tr}_3 = [\var{tr}_4, \var{tr}_5] = [\epsilon,\mathrm{Br}(\epsilon,1,[\epsilon,\mathrm{Br}(\epsilon,0, \epsilon)])]$ for example.
The first condition clearly holds, and the third condition can be solved by Tp-Var with
$\mu'_3 = \{ \var{xs} = \sem{a : x}^{-1} (\mu_2' \triangleleft \{ a = 1, x = [2,3] \}) \}$. So, let's focus on the
second condition (<ref>).
By Tp-BCon, this condition is reduced to

\begin{gather*}
\EvalRelBT{ \{a = 1, \dots\} }{ a  }{ 6 }{\var{tr}_4}{ \mu'_4 }
\end{gather*}

and checking whether $\var{tr}_5$ is the trace of the backward evaluation of $\var{append} \A x \A \var{ys}$
under $\{ x = [2,3], \var{ys} = [4,5], \dots \}$ for the updated view $[2]$ to yield $\mu'_5$ such that $\mu'_1 \uplus_{\{\var{xs},\var{ys}\}, \{a,x\}} \mu'_2  = \mu'_4 \lub \mu'_5$.
By Tp-Var, it is easy to see that the former holds with $\mu'_4 = \{ a = 6 \}$.
The latter holds if (and only if)[Similar to Footnote <ref>.]

\[
\EvalRelBT{\{\var{xs} = [2,3], \var{ys} = [4,5], \dots \}}{\var{appendBbody}}{[2]}{\var{tr}_5}{\mu'_6}
\]

holds with $\var{tr}_5 = \mathrm{Br}(\epsilon,1,[\epsilon, \var{tr}_6]) = \mathrm{Br}(\epsilon, 1,[\epsilon,\mathrm{Br}(\epsilon,0,\epsilon)])$ and $\mu'_5 = \{ x = \mu'_6(\var{xs}), \var{ys} = \mu'_6(\var{ys})\}$.
Again, in the backward evaluation of $\var{appendBbody}$, we know from the trace $\var{tr}_5$ that the second branch (cons case) must be chosen, and from the original environment $\{ \var{xs} = [2,3], \dots \}$ that the branch is the original one. Thus, the last rule used for the evaluation must be Tp-BCase1.

Thus, to make the above traced backward evaluation hold, it suffices (and needs) that the following conditions hold (again, we shall ignore irrelevant premises of Tp-BCase1).

\begin{gather*}
\EvalRelU{(\var{not} \circ \var{null}) \A [2] }{ \con{True} } \\
\EvalRelBT{ \{a = 2, x = [3], \var{ys} = [4,5], \dots\} }{ a \bxop{:} \var{appendB} \A x \A \var{ys} }{ [2] }{[\epsilon, \var{tr}_6]}{ \mu'_7 \uplus_{\{\var{ys}, \dots\}, \{a,x\}} \mu'_8 } \tag{\ensuremath{\ast\ast}}\label{prop:put2}\\
\EvalRelBT{ \{ \var{xs} = [2,3], \dots \} }{ \var{xs} }{ \sem{a : x}^{-1} (\mu_8' \triangleleft \{ a = 2, x = [3] \}) }{\epsilon}{ \mu'_9 }  \\
\mu'_6 = \mu'_7 \lub \mu'_9
\end{gather*}

The first condition clearly holds, and the third condition can be solved by Tp-Var with
$\mu'_9 = \{ \var{xs} = \sem{a : x}^{-1} (\mu_8' \triangleleft \{ a = 2, x = [3] \})$.
The second condition (<ref>) is further reduced to conditions:

\begin{gather*}
\EvalRelBT{ \{a = 2, \dots\} }{ a  }{ 2 }{\epsilon}{ \mu'_{10} } \\
\EvalRelBT{\{\var{xs} = [3], \var{ys} = [4,5], \dots \}}{\var{appendBbody}}{[\,]}{\var{tr}_6}{\mu'_{11}}\\
\mu'_7 \uplus_{\{\var{ys}, \dots\}, \{a,x\}} \mu'_8 = \mu'_{10} \lub \{ \var{x} = \mu'_{11}(\var{xs}), \var{ys} = \mu'_{11}(\var{ys}) \}\text{.}
\end{gather*}

Clearly, by Tp-Var, the first condition holds with $\mu'_{10} = \{ a = 2 \}$.
Thus, let's focus on the second condition.
Unlike the previous cases, the trace $\var{tr}_6 = \mathrm{Br}(\epsilon,0,\epsilon)$ says that the evaluation must use the first branch (nil case),
which is different from the original branch (taken under the environment $\{ \var{xs} = [3], \dots \}$).
Thus, the last rule used in the evaluation
\(
\EvalRelBT{\{\var{xs} = [3], \var{ys} = [4,5], \dots \}}{\var{appendBbody}}{[\,]}{\var{tr}_6}{\mu'_{11}}
\)
must be Tp-BCase2, meaning that branch switching happened. Since we have

\[
\EvalRelU{ (\lambda \dontcare. \lambda \dontcare.\, [\,]) \A [3] \A [\,] }{ [\,] }
\]

we then check other premises of the rule instance (again, we shall ignore the irrelevant ones):

\begin{gather*}
\EvalRelU{(\var{not} \circ \var{null}) \A [\,]}{\con{False}} \\
\EvalRelU{(\var{const} \A \con{True}) \A [\,]}{\con{True}} \\
\EvalRelBT{ \{ \var{ys} = [4,5], \dots \} }{ \var{ys} }{ [\,] }{ \epsilon }{ \mu'_{12} \uplus_{\{ \var{ys}, \dots\}, \emptyset} \emptyset} \\
\EvalRelBT{ \{ \var{xs} = [3], \dots \}  }{ \var{xs} }{ \sem{ [\,] }^{-1}(\emptyset \triangleleft \emptyset) }{ \epsilon }{ \mu'_{13} }\\
\mu'_{11} = \mu'_{12} \lub \mu'_{13}\text{.}
\end{gather*}

The first two clearly hold, and by Tp-Var, the third and forth ones hold with  $\mu'_{12} = \{ \var{ys} = [\,] \}$ and $\mu'_{13} = \{ \var{xs} = [\,] \}$.
Thus, we have $\mu'_{11} = \{ \var{xs} = [\,], \var{ys} = [\,] \}$ to satisfy the fifth condition.
Then, we can solve the constraints on environments obtained so far as:
$\mu'_8 = \{ a = 2, x = [\,] \}$,
$\mu'_7 = \{ \var{ys} = [\,] \}$,
$\mu'_9 = \{ \var{xs} = [2] \}$,
$\mu'_6 = \{ \var{xs} = [2], \var{ys} = [\,] \}$,
$\mu'_5 = \{ x = [2], \var{ys} = [\,] \}$,
$\mu'_1 = \{ \var{ys} = [\,] \}$,
$\mu'_2 = \{ a = 6, x = [2] \}$, and
$\mu'_3 = \{ \var{xs} = [6,2] \}$. Now, we are ready to check $\mu' = \{ \var{xs} = [6,2], \var{ys} = [\,] \} = \mu'_1 \lub \mu'_3$ to conclude (<ref>).

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Abate, Bessa, Cattaruzza, Cordeiro, David,
Kesseli, Kroening, and PolgreenAbate et al2017]
authorpersonAlessandro Abate, personIury
Bessa, personDario Cattaruzza, personLucas C.
Cordeiro, personCristina David, personPascal
Kesseli, personDaniel Kroening, and personElizabeth
Polgreen. year2017.
Automated Formal Synthesis of Digital Controllers
for State-Space Physical Plants. In booktitleComputer Aided
Verification - 29th International Conference, CAV 2017, Heidelberg,
Germany, July 24-28, 2017, Proceedings, Part I
(seriesLecture Notes in Computer Science,
Vol. volume10426), editorpersonRupak
Majumdar and personViktor Kuncak (Eds.).
publisherSpringer, pages462–482.

[Abate, David, Kesseli, Kroening, and
PolgreenAbate et al2018]
authorpersonAlessandro Abate, personCristina
David, personPascal Kesseli, personDaniel Kroening,
and personElizabeth Polgreen. year2018.
Counterexample Guided Inductive Synthesis Modulo
Theories. In booktitleComputer Aided Verification - 30th
International Conference, CAV 2018, Held as Part of the Federated Logic
Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I
(seriesLecture Notes in Computer Science,
Vol. volume10981), editorpersonHana
Chockler and personGeorg Weissenbacher (Eds.).
publisherSpringer, pages270–288.

[Albarghouthi, Gulwani, and
KincaidAlbarghouthi et al2013]
authorpersonAws Albarghouthi, personSumit
Gulwani, and personZachary Kincaid.
Recursive Program Synthesis. In
booktitleComputer Aided Verification - 25th International
Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013.
Proceedings (seriesLecture Notes in Computer Science,
Vol. volume8044), editorpersonNatasha
Sharygina and personHelmut Veith (Eds.).
publisherSpringer, pages934–950.

[Almendros-Jiménez and
VidalAlmendros-Jiménez and Vidal2006]
authorpersonJesús Manuel
Almendros-Jiménez and personGermán Vidal.
Automatic Partial Inversion of Inductively
Sequential Functions. In booktitleImplementation and
Application of Functional Languages, 18th International Symp osium, IFL
2006, Budapest, Hungary, September 4-6, 2006, Revised Selected Papers
(seriesLecture Notes in Computer Science,
Vol. volume4449),
editorpersonZoltán Horváth,
personViktória Zsók, and personAndrew
Butterfield (Eds.). publisherSpringer,

[Bancilhon and SpyratosBancilhon and
authorpersonFrançois Bancilhon and
personNicolas Spyratos. year1981.
Update Semantics of Relational Views.
journalACM Trans. Database Syst.
volume6, number4 (year1981),

[Bohannon, Foster, Pierce, Pilkiewicz, and
SchmittBohannon et al2008]
authorpersonAaron Bohannon, personJ. Nathan
Foster, personBenjamin C. Pierce, personAlexandre
Pilkiewicz, and personAlan Schmitt.
Boomerang: resourceful lenses for string data. In
booktitleProceedings of the 35th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2008, San Francisco,
California, USA, January 7-12, 2008,
editorpersonGeorge C. Necula and
personPhilip Wadler (Eds.). publisherACM,

[Chong, Cook, Kallas, Khazem, Monteiro,
Schwartz-Narbonne, Tasiran, Tautschnig, and TuttleChong
et al2020]
authorpersonNathan Chong, personByron Cook,
personKonstantinos Kallas, personKareem Khazem,
personFelipe R. Monteiro, personDaniel
Schwartz-Narbonne, personSerdar Tasiran,
personMichael Tautschnig, and personMark R.
Tuttle. year2020.
Code-level model checking in the software
development workflow. In booktitleICSE-SEIP 2020: 42nd
International Conference on Software Engineering, Software Engineering in
Practice, Seoul, South Korea, 27 June - 19 July, 2020,
editorpersonGregg Rothermel and
personDoo-Hwan Bae (Eds.). publisherACM,

[Damas and MilnerDamas and Milner1982]
authorpersonLuís Damas and
personRobin Milner. year1982.
Principal Type-Schemes for Functional Programs. In
booktitleConference Record of the Ninth Annual ACM
Symposium on Principles of Programming Languages, Albuquerque, New Mexico,
USA, January 1982, editorpersonRichard A. DeMillo
(Ed.). publisherACM Press, pages207–212.

[David, Kesseli, Kroening, and LewisDavid
et al2018]
authorpersonCristina David, personPascal
Kesseli, personDaniel Kroening, and personMatt
Lewis. year2018.
Program Synthesis for Program Analysis.
journalACM Trans. Program. Lang. Syst.
volume40, number2 (year2018),

[David, Kroening, and LewisDavid
et al2015]
authorpersonCristina David, personDaniel
Kroening, and personMatt Lewis.
Unrestricted Termination and Non-termination
Arguments for Bit-Vector Programs. In booktitleProgramming
Languages and Systems - 24th 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-18, 2015. Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume9032), editorpersonJan Vitek
(Ed.). publisherSpringer, pages183–204.

[Davies and PfenningDavies and
authorpersonRowan Davies and personFrank
Pfenning. year2001.
A modal analysis of staged computation.
journalJ. ACM volume48,
number3 (year2001), pages555–604.

[de Jonge and Visserde Jonge and
authorpersonMaartje de Jonge and
personEelco Visser. year2011.
An Algorithm for Layout Preservation in Refactoring
Transformations. In booktitleSoftware Language Engineering
- 4th International Conference, SLE 2011, Braga, Portugal, July 3-4, 2011,
Revised Selected Papers (seriesLecture Notes in Computer
Science, Vol. volume6940),
editorpersonAnthony M. Sloane and
personUwe Aßmann (Eds.). publisherSpringer,

[Feng, Martins, Wang, Dillig, and RepsFeng
et al2017]
authorpersonYu Feng, personRuben Martins,
personYuepeng Wang, personIsil Dillig, and
personThomas W. Reps. year2017.
Component-based synthesis for complex APIs. In
booktitleProceedings of the 44th ACM SIGPLAN Symposium
on Principles of Programming Languages, POPL 2017, Paris, France, January
18-20, 2017, editorpersonGiuseppe Castagna and
personAndrew D. Gordon (Eds.). publisherACM,

[Feser, Chaudhuri, and DilligFeser
et al2015]
authorpersonJohn K. Feser, personSwarat
Chaudhuri, and personIsil Dillig.
Synthesizing data structure transformations from
input-output examples. In booktitleProceedings of the 36th
ACM SIGPLAN Conference on Programming Language Design and Implementation,
Portland, OR, USA, June 15-17, 2015,
editorpersonDavid Grove and
personStephen M. Blackburn (Eds.). publisherACM,

[Fischer, Kiselyov, and ShanFischer
et al2011]
authorpersonSebastian Fischer, personOleg
Kiselyov, and personChung-chieh Shan.
Purely functional lazy nondeterministic
journalJ. Funct. Program. volume21,
number4-5 (year2011), pages413–465.

[Foster, Greenwald, Moore, Pierce, and
SchmittFoster et al2007]
authorpersonJ. Nathan Foster,
personMichael B. Greenwald, personJonathan T. Moore,
personBenjamin C. Pierce, and personAlan Schmitt.
Combinators for bidirectional tree transformations:
A linguistic approach to the view-update problem.
journalACM Trans. Program. Lang. Syst.
volume29, number3 (year2007).

[Foster, Pilkiewicz, and PierceFoster
et al2008]
authorpersonJ. Nathan Foster,
personAlexandre Pilkiewicz, and personBenjamin C.
Pierce. year2008.
Quotient lenses. In
booktitleProceeding of the 13th ACM SIGPLAN
international conference on Functional programming, ICFP 2008, Victoria,
BC, Canada, September 20-28, 2008, editorpersonJames
Hook and personPeter Thiemann (Eds.).
publisherACM, pages383–396.

[Glück and KawabeGlück and
authorpersonRobert Glück and
personMasahiko Kawabe. year2005.
Revisiting an automatic program inverter for Lisp.
journalSIGPLAN Notices volume40,
number5 (year2005), pages8–17.

[Gomard and JonesGomard and Jones1991]
authorpersonCarsten K. Gomard and
personNeil D. Jones. year1991.
A Partial Evaluator for the Untyped
journalJ. Funct. Program. volume1,
number1 (year1991), pages21–69.

authorpersonDavid Gries.
booktitleThe Science of Programming.
publisherSpringer, Heidelberg, Chapter 21 Inverting

authorpersonSumit Gulwani.
Automating string processing in spreadsheets using
input-output examples. In booktitleProceedings of the 38th
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL 2011, Austin, TX, USA, January 26-28, 2011,
editorpersonThomas Ball and personMooly
Sagiv (Eds.). publisherACM, pages317–330.

authorpersonStephen J. Hegner.
Foundations of Canonical Update Support for Closed
Database Views. In booktitleICDT
(seriesLecture Notes in Computer Science,
Vol. volume470), editorpersonSerge
Abiteboul and personParis C. Kanellakis (Eds.).
publisherSpringer, pages422–436.

[Hofmann, Pierce, and WagnerHofmann
et al2011]
authorpersonMartin Hofmann,
personBenjamin C. Pierce, and personDaniel Wagner.
Symmetric lenses. In
booktitleProceedings of the 38th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2011, Austin, TX,
USA, January 26-28, 2011, editorpersonThomas Ball
and personMooly Sagiv (Eds.). publisherACM,

[Hu and KoHu and Ko2016]
authorpersonZhenjiang Hu and
personHsiang-Shang Ko. year2016.
Principles and Practice of Bidirectional
Programming in BiGUL. In booktitleBidirectional
Transformations - International Summer School, Oxford, UK, July 25-29, 2016,
Tutorial Lectures (seriesLecture Notes in Computer
Science, Vol. volume9715),
editorpersonJeremy Gibbons and
personPerdita Stevens (Eds.). publisherSpringer,

[Jha, Gulwani, Seshia, and TiwariJha
et al2010]
authorpersonSusmit Jha, personSumit
Gulwani, personSanjit A. Seshia, and personAshish
Tiwari. year2010.
Oracle-guided component-based program synthesis.
In booktitleProceedings of the 32nd ACM/IEEE International
Conference on Software Engineering - Volume 1, ICSE 2010, Cape Town, South
Africa, 1-8 May 2010, editorpersonJeff Kramer,
personJudith Bishop, personPremkumar T. Devanbu,
and personSebastián Uchitel (Eds.).
publisherACM, pages215–224.

authorpersonSusumu Katayama.
Systematic search for lambda expressions. In
booktitleRevised Selected Papers from the Sixth Symposium on
Trends in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24
September 2005 (seriesTrends in Functional Programming,
Vol. volume6), editorpersonMarko C. J. D.
van Eekelen (Ed.). publisherIntellect,

[Kiselyov and ThompsonKiselyov and
editorpersonOleg Kiselyov and
personSimon J. Thompson (Eds.). year2012.
booktitleProceedings of the ACM SIGPLAN 2012
Workshop on Partial Evaluation and Program Manipulation, PEPM 2012,
Philadelphia, Pennsylvania, USA, January 23-24, 2012.

[Kneuss, Kuraj, Kuncak, and SuterKneuss
et al2013]
authorpersonEtienne Kneuss, personIvan
Kuraj, personViktor Kuncak, and personPhilippe
Suter. year2013.
Synthesis modulo recursive functions. In
booktitleProceedings 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-31, 2013, editorpersonAntony L.
Hosking, personPatrick Th. Eugster, and
personCristina V. Lopes (Eds.). publisherACM,

[Ko, Zan, and HuKo et al2016]
authorpersonHsiang-Shang Ko, personTao
Zan, and personZhenjiang Hu. year2016.
BiGUL: a formally verified core language for
putback-based bidirectional programming. In
booktitleProceedings of the 2016 ACM SIGPLAN Workshop on
Partial Evaluation and Program Manipulation, PEPM 2016, St. Petersburg, FL,
USA, January 20 - 22, 2016, editorpersonMartin
Erwig and personTiark Rompf (Eds.).
publisherACM, pages61–72.

authorpersonRichard E. Korf.
Inversion of Applicative Programs. In
editorpersonPatrick J. Hayes (Ed.).
publisherWilliam Kaufmann, pages1007–1009.

[Kort and LämmelKort and
authorpersonJan Kort and personRalf
Lämmel. year2003.
Parse-Tree Annotations Meet Re-Engineering
Concerns. In booktitle3rd IEEE International Workshop on
Source Code Analysis and Manipulation (SCAM 2003), 26-27 September 2003,
Amsterdam, The Netherlands. publisherIEEE Computer Society,

[Koukoutos, Kneuss, and KuncakKoukoutos
et al2016]
authorpersonManos Koukoutos, personEtienne
Kneuss, and personViktor Kuncak.
An Update on Deductive Synthesis and Repair in the
Leon Tool. In booktitleProceedings Fifth Workshop on
Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016
(seriesEPTCS, Vol. volume229),
editorpersonRuzica Piskac and
personRayna Dimitrova (Eds.). pages100–111.

[Lubin, Collins, Omar, and ChughLubin
et al2020]
authorpersonJustin Lubin, personNick
Collins, personCyrus Omar, and personRavi Chugh.
Program sketching with live bidirectional
journalProc. ACM Program. Lang.
volume4, numberICFP (year2020),

authorpersonChristopher Lutz.
titleJanus: a time-reversible language.
Letter to R. Landauer. Available on:

[Maina, Miltner, Fisher, Pierce, Walker, and
ZdancewicMaina et al2018]
authorpersonSolomon Maina, personAnders
Miltner, personKathleen Fisher, personBenjamin C.
Pierce, personDavid Walker, and personSteve
Zdancewic. year2018.
Synthesizing quotient lenses.
journalProc. ACM Program. Lang.
volume2, numberICFP (year2018),

[Matsuda, Hu, Nakano, Hamana, and
TakeichiMatsuda et al2007]
authorpersonKazutaka Matsuda,
personZhenjiang Hu, personKeisuke Nakano,
personMakoto Hamana, and personMasato Takeichi.
Bidirectionalization transformation based on
automatic derivation of view complement functions. In
booktitleProceedings of the 12th ACM SIGPLAN
International Conference on Functional Programming, ICFP 2007, Freiburg,
Germany, October 1-3, 2007, editorpersonRalf Hinze
and personNorman Ramsey (Eds.). publisherACM,

[Matsuda, Inaba, and NakanoMatsuda
et al2012]
authorpersonKazutaka Matsuda, personKazuhiro
Inaba, and personKeisuke Nakano.
Polynomial-time inverse computation for
accumulative functions with multiple data traversals, See
DBLP:conf/pepm/2012, pages5–14.

[Matsuda, Mu, Hu, and TakeichiMatsuda
et al2010]
authorpersonKazutaka Matsuda,
personShin-Cheng Mu, personZhenjiang Hu, and
personMasato Takeichi. year2010.
A Grammar-Based Approach to Invertible Programs.
In booktitleESOP (seriesLecture Notes in
Computer Science, Vol. volume6012),
editorpersonAndrew D. Gordon (Ed.).
publisherSpringer, pages448–467.

[Matsuda and WangMatsuda and Wang2015a]
authorpersonKazutaka Matsuda and
personMeng Wang. year2015a.
Applicative bidirectional programming with lenses.
In booktitleProceedings of the 20th ACM SIGPLAN
International Conference on Functional Programming, ICFP 2015, Vancouver,
BC, Canada, September 1-3, 2015,
editorpersonKathleen Fisher and
personJohn H. Reppy (Eds.). publisherACM,

[Matsuda and WangMatsuda and Wang2015b]
authorpersonKazutaka Matsuda and
personMeng Wang. year2015b.
"Bidirectionalization for free" for monomorphic
journalSci. Comput. Program.
volume111 (year2015), pages79–109.

[Matsuda and WangMatsuda and Wang2018a]
authorpersonKazutaka Matsuda and
personMeng Wang. year2018a.
Applicative bidirectional programming: Mixing
lenses and semantic bidirectionalization.
journalJ. Funct. Program.  volume28
(year2018), pagese15.

[Matsuda and WangMatsuda and Wang2018b]
Matsuda   Wang:2018:HOBiT
authorpersonKazutaka Matsuda and
personMeng Wang. year2018b.
HOBiT: Programming Lenses Without Using Lens
Combinators. In booktitleProgramming Languages and Systems
- 27th 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-20, 2018, Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume10801), editorpersonAmal
Ahmed (Ed.). publisherSpringer, pages31–59.

[Matsuda and WangMatsuda and Wang2020]
authorpersonKazutaka Matsuda and
personMeng Wang. year2020.
Sparcl: a language for partially-invertible
journalProc. ACM Program. Lang.
volume4, numberICFP (year2020),

[Miltner, Fisher, Pierce, Walker, and
ZdancewicMiltner et al2018]
authorpersonAnders Miltner, personKathleen
Fisher, personBenjamin C. Pierce, personDavid
Walker, and personSteve Zdancewic.
Synthesizing bijective lenses.
journalProc. ACM Program. Lang.
volume2, numberPOPL (year2018),

[Miltner, Maina, Fisher, Pierce, Walker, and
ZdancewicMiltner et al2019]
authorpersonAnders Miltner, personSolomon
Maina, personKathleen Fisher, personBenjamin C.
Pierce, personDavid Walker, and personSteve
Zdancewic. year2019.
Synthesizing symmetric lenses.
journalProc. ACM Program. Lang.
volume3, numberICFP (year2019),

[Nishida, Sakai, and SakabeNishida
et al2005]
authorpersonNaoki Nishida, personMasahiko
Sakai, and personToshiki Sakabe.
Partial Inversion of Constructor Term Rewriting
Systems. In booktitleTerm Rewriting and Applications, 16th
International Conference, RTA 2005, Nara, Japan, April 19-21, 2005,
Proceedings (seriesLecture Notes in Computer Science,
Vol. volume3467),
editorpersonJürgen Giesl (Ed.).
publisherSpringer, pages264–278.

[Nishida and VidalNishida and Vidal2011]
authorpersonNaoki Nishida and
personGermán Vidal. year2011.
Program Inversion for Tail Recursive Functions. In
booktitleProceedings of the 22nd International Conference on
Rewriting Techniques and Applications, RTA 2011, May 30 - June 1, 2011,
Novi Sad, Serbia (seriesLIPIcs,
Vol. volume10), editorpersonManfred
Schmidt-Schauß (Ed.). publisherSchloss Dagstuhl -
Leibniz-Zentrum für Informatik, pages283–298.

[Osera and ZdancewicOsera and
authorpersonPeter-Michael Osera and
personSteve Zdancewic. year2015.
Type-and-example-directed program synthesis. In
booktitleProceedings of the 36th ACM SIGPLAN Conference
on Programming Language Design and Implementation, Portland, OR, USA, June
15-17, 2015, editorpersonDavid Grove and
personStephen M. Blackburn (Eds.). publisherACM,

[Pacheco, Hu, and FischerPacheco
et al2014]
authorpersonHugo Pacheco, personZhenjiang
Hu, and personSebastian Fischer.
Monadic combinators for "Putback" style
bidirectional programming. In booktitleProceedings of the
ACM SIGPLAN 2014 workshop on Partial evaluation and program manipulation,
PEPM 2014, January 20-21, 2014, San Diego, California, USA,
editorpersonWei-Ngan Chin and
personJurriaan Hage (Eds.). publisherACM,

[Pombrio and KrishnamurthiPombrio and
authorpersonJustin Pombrio and
personShriram Krishnamurthi. year2014.
Resugaring: lifting evaluation sequences through
syntactic sugar. In booktitleACM SIGPLAN Conference on
Programming Language Design and Implementation, PLDI '14, Edinburgh, United
Kingdom - June 09 - 11, 2014, editorpersonMichael
F. P. O'Boyle and personKeshav Pingali (Eds.).
publisherACM, pages361–371.

authorpersonJohn C. Reynolds.
Types, Abstraction and Parametric Polymorphism. In
booktitleInformation Processing 83, Proceedings of the
IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983,
editorpersonR. E. A. Mason (Ed.).
publisherNorth-Holland/IFIP, pages513–523.

[Smith and AlbarghouthiSmith and
authorpersonCalvin Smith and personAws
Albarghouthi. year2019.
Program Synthesis with Equivalence Reduction. In
booktitleVerification, Model Checking, and Abstract
Interpretation - 20th International Conference, VMCAI 2019, Cascais,
Portugal, January 13-15, 2019, Proceedings (seriesLecture
Notes in Computer Science, Vol. volume11388),
editorpersonConstantin Enea and
personRuzica Piskac (Eds.). publisherSpringer,

authorpersonArmando Solar-Lezama.
The Sketching Approach to Program Synthesis. In
booktitleProgramming Languages and Systems, 7th Asian
Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume5904), editorpersonZhenjiang
Hu (Ed.). publisherSpringer, pages4–13.

[Solar-Lezama, Jones, and
BodíkSolar-Lezama et al2008]
authorpersonArmando Solar-Lezama,
personChristopher Grant Jones, and personRastislav
Bodík. year2008.
Sketching concurrent data structures. In
booktitlePLDI. pages136–148.

[Srivastava, Gulwani, Chaudhuri, and
FosterSrivastava et al2011]
authorpersonSaurabh Srivastava, personSumit
Gulwani, personSwarat Chaudhuri, and
personJeffrey S. Foster. year2011.
Path-based inductive synthesis for program
inversion. In booktitleProceedings of the 32nd ACM
SIGPLAN Conference on Programming Language Design and Implementation,
PLDI 2011, San Jose, CA, USA, June 4-8, 2011,
editorpersonMary W. Hall and
personDavid A. Padua (Eds.). publisherACM,

authorpersonPerdita Stevens.
booktitleA Landscape of Bidirectional Model
publisherSpringer Berlin Heidelberg,
addressBerlin, Heidelberg, pages408–424.

authorpersonJanis Voigtländer.
Bidirectionalization for Free! (Pearl). In
booktitleProceedings of the 36th Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (Savannah, GA, USA)
(seriesPOPL '09). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

authorpersonJanis Voigtländer.
Bidirectionalization for free! (Pearl). In
booktitleProceedings of the 36th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA,
USA, January 21-23, 2009, editorpersonZhong Shao
and personBenjamin C. Pierce (Eds.).
publisherACM, pages165–176.

authorpersonJanis Voigtländer.
Ideas for connecting inductive program synthesis
and bidirectionalization, See DBLP:conf/pepm/2012,

[Voigtländer, Hu, Matsuda, and
WangVoigtländer et al2013]
authorpersonJanis Voigtländer,
personZhenjiang Hu, personKazutaka Matsuda, and
personMeng Wang. year2013.
Enhancing semantic bidirectionalization via shape
bidirectionalizer plug-ins.
journalJ. Funct. Program. volume23,
number5 (year2013), pages515–551.

authorpersonPhilip Wadler.
Theorems for Free!. In
booktitleProceedings of the fourth international conference
on Functional programming languages and computer architecture, FPCA 1989,
London, UK, September 11-13, 1989,
editorpersonJoseph E. Stoy (Ed.).
publisherACM, pages347–359.

authorpersonPhilip Wadler.
Deforestation: Transforming Programs to Eliminate
journalTheor. Comput. Sci. volume73,
number2 (year1990), pages231–248.

[Yamaguchi, Matsuda, David, and WangYamaguchi
et al2021]
authorpersonMasaomi Yamaguchi,
personKazutaka Matsuda, personCristina David, and
personMeng Wang. year2021.
Synbit: Synthesizing Bidirectional Programs
using Unidirectional Sketches.
journalCoRR  volumeabs/2108.13783

[Yokoyama, Axelsen, and GlückYokoyama
et al2008]
authorpersonTetsuo Yokoyama,
personHolger Bock Axelsen, and personRobert
Glück. year2008.
Principles of a reversible programming language.
In booktitleProceedings of the 5th Conference on Computing
Frontiers, 2008, Ischia, Italy, May 5-7, 2008,
editorpersonAlex Ramírez,
personGianfranco Bilardi, and personMichael
Gschwind (Eds.). publisherACM, pages43–54.

[Yokoyama, Axelsen, and GlückYokoyama
et al2011]
authorpersonTetsuo Yokoyama,
personHolger Bock Axelsen, and personRobert
Glück. year2011.
Towards a Reversible Functional Language. In
booktitleRC (seriesLecture Notes in
Computer Science, Vol. volume7165),
editorpersonAlexis De Vos and
personRobert Wille (Eds.). publisherSpringer,