Dependent Bijective Lenses

April 17, 2020
3:00
Zoom
Speaker: Jeanne-Marie Musca
Host: Kathleen Fisher

Abstract

I present my work on formalizing and synthesizing dependent bijective lenses. Bijective lenses encode two functions: one that translates data from format A to format B and the other that translates the data from B back to A. My work extends two projects on bijective lenses: Boomerang and Optician. Boomerang is a programming language for writing lenses that are proven to behave as expected, and Optician synthesizes Boomerang lenses based on format descriptions. Boomerang's formalism, however, limits the formats to those that can be represented by regular expressions, which excludes, for instance, formats with internal dependencies. So, I am extending Boomerang with well-behaved lenses that operate between formats that have internal dependencies, specifically those that can be represented with PCRE backreferences. For example, take a bibliography whose entries are labelled by a tag that concatenates the author's last name and the published year. Dependent bijective lenses can be used to translate this bibliography between BibTeX and EndNote formats, while enforcing that the tags remain consistent with the entries they label. I present my on-going work on developing a formalism and logical framework that allows me to prove that dependent bijective lenses are well-behaved. I also discuss extending Optician to synthesize these lenses. Finally, I outline ways in which the framework could be extended to represent more complex internal dependencies, such as data with fields that indicate the size of the other parts of the data.

Join Zoom Meeting

https://tufts.zoom.us/j/770993886

Meeting ID: 770 993 886

See the colloquium announcement email for the Zoom password.