Why $\lambda$‽

Lady Margaret Hall, Oxford, UK
25th to 29th July 2016
http://www.cs.ox.ac.uk/projects/tlcbx/ssbx/

TOPIC

Bidirectional transformations (BX) are means of maintaining consistency between multiple information sources: when one source is edited, the others may need updating to restore consistency. BX have applications in databases, user interface design, model-driven development, and many other domains. This summer school is one of the closing activities on the "Theory of Least Change for BX" project at Oxford and Edinburgh. It brings together leading researchers in BX, spanning theory and
practice, for a week of lectures in beautiful Oxford. It will be aimed at doctoral students in computer science, but will also be suitable for strong master's students and for researchers.

Read more »

Labels: advertising, bidirectional computation

I am currently advertising two PhD studentships, on topics spanning programming languages, provenance, and data management, to start in fall 2016.

Both of these studentships are fully funded for applicants of any nationality (in contrast to many UK PhD studentships which are only funded up to the UK/EU tuition level, and do not cover full tuition fees for students from outside the European Union.)
Read more »

Labels: advertising, bidirectional computation, databases, functional programming, logic programming, programming languages, provenance

Thanks to Matt Might for some very kind words on our paper "Reflections on monadic lenses", recently posted to arXiv.org and scheduled to appear in April as part of an upcoming Festschrift for Phil Wadler.

A great review of bidirectional programming with (monadic) effects: https://t.co/rea2JJcTnX by @jer_gib & co.

— Matt Might (@mattmight) January 12, 2016

Labels: bidirectional computation, monads

Edit Lenses
M. Hofmann, B. Pierce, and D. Wagner
Proceedings of POPL 2012, p. 495-508.


I previously wrote about Diskin et al.'s delta lenses. That paper explores one approach to bidirectional transformations that takes into account information about the update process changing one state to another.

In this paper, Pierce et al. explore what they call edit lenses. A delta lens considers a state space as a category, with the arrows of the category being updates describing how to get from one state to another. An edit lens, by contrast, considers a state space acted upon by a monoid (this idea appears in previous work on algebraic foundations of bidirectional transformations by Stevens, and was mentioned in Pierce et al.'s Symmetric Lenses paper as a natural next step).

Read more »

Labels: bidirectional computation, incremental computation, programming languages

From State- to Delta-Based Bidirectional Model Transformations: the Asymmetric Case
Zinovy Diskin, Yingfei Xiong, and Krzysztof Czarnecki
Journal of Object Technology 10(6):1-25, 2011

This paper is the journal version of an ICMT 2010 paper, which I had read a few years ago. The journal version is sufficiently different to make it worthwhile to read if you'd already read the conference version; I had particular trouble with the small figures/examples in the conference version, and this one is much better in that respect.

The idea is to revisit the notion of "lens" or (asymmetric) bidirectional transformation, introduced in now-classic work by Foster et al. (POPL 2005, TOPLAS 2007). Basically, a lens is a pair of functions
$\newcommand{\AA}{\mathbf{A}}$
$\newcommand{\BB}{\mathbf{B}}$

\[
\begin{eqnarray*}
get &:& \AA \to \BB\\
put &:& \AA\times \BB \to \AA
\end{eqnarray*}
\]

where the idea is, $get$ maps some source data $A \in \AA$ to a "view" $B \in \BB,ドル and $put$ takes a (possibly updated) $B' \in \BB$ and the original $A \in \AA$ and produces a corresponding $A' \in \AA$. These are expected to satisfy some basic consistency laws.


Read more »

Labels: bidirectional computation, incremental computation