Characterizations of Partial Well-Behaved Lenses
This program is tentative and subject to change.
Foster et al. proposed a linguistic approach to the bidirectional transformation, with lens. A lens is a pair of two functions, one is a forward transformation called get which produces a target view from an original source, and the other is a backward transformation called put which updates the original source to a new one with an updated view. The get and put functions depend on each other to be consistent. A lens is called well-behaved if it satisfies two lens laws, GetPut and PutGet. Every put function uniquely determines a get function if it exists, as far as the get and put functions form a well-behaved lens. Fischer et al. found the conditions of a put function under which the corresponding get function exists, where both get and put functions are supposed to be total. In this paper, we consider the case where get and put functions are possibly partial. We show that almost the same conditions as the ones given by Fischer et al. work well when only a put function is possibly partial, while they do not work when a get function is also possibly partial. In order to have similar results, we propose a new lens law for the case where both get and put functions are possibly partial.
This program is tentative and subject to change.
Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change
16:00 - 17:30 | |||
16:00 15mShort-paper | Type-Sensitive Algebraic Macros (Short Paper)Remote PEPM File Attached | ||
16:15 30mResearch paper | Characterizations of Partial Well-Behaved Lenses PEPM Keishi HASHIBA The University of Osaka, Keisuke Nakano Tohoku University, Kazuyuki Asada Tohoku University, Kentaro Kikuchi Tohoku University | ||
16:45 40mPanel | Semantics-based program manipulation in the age of LLMs PEPM William J. Bowman University of British Columbia, Brigitte Pientka McGill University, Satnam Singh Groq | ||
17:25 5mDay closing | Farewell PEPM Y. Annie Liu Stony Brook University |