RESEARCH
Program Synthesis: Lens Synthesis
Lenses are programs that can be run both “front to back” and “back to front,” allowing updates to either their source or their target data to be transferred to the other. Since their introduction by Foster et al., lenses have been extensively studied, extended, and applied. In this work, we study how techniques from type-directed program synthesis can be used to efficiently synthesize a variety of lenses from format descriptions of the source and target and a small number of examples.
People
- Solomon Maina
- Anders Miltner
- JM Musca
- Benjamin C. Pierce
- David Walker
- Steve Zdancewic
Papers
- A. Miltner, S. Maina, K. Fisher, B. C. Pierce, D. Walker, and S. Zdancewic. Synthesizing symmetric lenses. Proc. ACM Program. Lang., 3(ICFP):95:1–95:28, July 2019.
- S. Maina, A. Miltner, K. Fisher, B. C. Pierce, D. Walker, and S. Zdancewic. Synthesizing quotient lenses. In ICFP ’18: Proceedings of the 23rd ACM SIGPLAN International Conference on Functional Programming, 2018.
- A. Miltner, K. Fisher, B. C. Pierce, D. Walker, and S. Zdancewic. Synthesizing bijective lenses. In POPL ’18: Proceedings of the 45th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2018.