Accepted Papers and Talks

Full Papers

ASN.1 Encoding Schemes Done Right Using CMPCT

Mark Tullsen (Galois, Inc.)

Abstract Syntax Notation One (ASN.1) is a ubiquitous data description language for defining data that can be serialized and deserialized across platforms. ASN.1 supports multiple encoding schemes: each encoding scheme specifies the rules for representing abstract values as a sequence of bytes. Some of the more common encoding schemes are Basic Encoding Rules (BER), Distinguished Encoding Rules (DER), Packed Encoding Rules (PER), and XML Encoding Rules (XER). In the process of validating the correctness of an ASN.1 encoder/decoder pair for the J2735 standard (Dedicated Short Range Communications Message Set for Vehicle to Vehicle communications), we have designed an intermediate language for describing ASN.1 types as well as ASN.1 encoding schemes. Our intermediate language, CMPCT, demonstrates the elegance of using “bidirectional transformation” methods. CMPCT allows one to create arbitrary encoding schemes that are correct by construction.

Lenses and Learners

Brendan Fong (Massachusetts Institute of Technology) and Michael Johnson (Macquarie University)

Lenses are a well-established structure for modelling bidirectional transformations, such as the interactions between a database and a view of it. Lenses may be symmetric or asymmetric, and may be composed, forming the morphisms of a monoidal category. More recently, the notion of a learner has been proposed: these provide a compositional way of modelling supervised learning algorithms, and again form the morphisms of a monoidal category. In this paper, we show that the two concepts are tightly linked. We show both that there is a faithful, identity-on-objects monoidal functor embedding a category of asymmetric lenses into the category of learners, and furthermore there is such a functor embedding the category of learners into a category of symmetric lenses.

Multicategories of Multiary Lenses

Michael Johnson (Macquarie University) and Robert Rosebrugh (Mount Allison University)

Bidirectional transformations have always been intended to, in combination, support complex transformations among multiple data sources, and in their applications dating back to before they were even called bidirectional transformations, they have done so. Nevertheless, only recently [Diskin et al, 2018, see also Dagstuhl, 2018] have lens-like definitions of multidirectional transformations been presented, encompassing both a “propagation” form (in the style of the original symmetric lenses of Hofmann, Pierce and Wagner) and a “wide span” form (in the style of the spans of d-lenses of Johnson and Rosebrugh). These “multiary lenses” raise a number of new challenges that are addressed in this paper. First, in common with classical symmetric lenses, they need to be studied modulo equivalence relations that factor out differences in hidden data and declare two lenses to be equivalent if their observable behaviours correspond. Then, modulo those equivalence relations the precise relationship between the propagation style lenses and the wide span lenses needs to be established. All of this is carried through here. But more significantly, the compositions of multiary lenses proposed to date have suffered various limitations: well-behaved amendment lenses don't necessarily compose to give well-behaved amendment lenses; technical conditions on model spaces can interfere with composition; junction conditions needed to be introduced because certain kinds of compositions of multiary lenses might not always be defined; and in any case, composition of multiary lenses comes with unusual challenges and can't be expected to form a category structure since when there are more than two data sources there are not even single notions of domain or codomain for multiary lenses. In this paper we introduce a class of asymmetric amendment lenses called spg-lenses (stable put-get lenses) which is more general than well-behaved amendment lenses, but is closed under composition, and we show how to use spg-lenses to capture, via wide spans, a wide class of multidirectional transformations which compose well and form a well-known and long-standing structure, a multicategory — a multicategory of multiary lenses.

Tool Paper

Incremental Bidirectional Model Transformation with eMoflon::IBeX

Nils Weidmann (Paderborn University), Anthony Anjorin (Paderborn University), Lars Fritsche (TU Darmstadt), Gergely Varró, Andy Schürr (TU Darmstadt), and Erhan Leblebici (TU Darmstadt)

Consistency management is a crucial task in the context of model-driven engineering, as multiple teams of domain experts must be able to work concurrently with different models. Triple Graph Grammars (TGGs) are a well-known approach to consistency management with the unique advantage of being declarative enough to address multiple consistency management tasks with the same specification, while still achieving an acceptable level of scalability for realistic application scenarios. Although there have been numerous TGG-based tools in the past, to the best of our knowledge, there exists no TGG-based tool that addresses multiple consistency management tasks in a conceptually and technically uniform manner. We argue that this is the reason why TGG-based tools typically do not maintain the same level of support for more than one or two such tasks. In this paper, we present eMoflon::IBeX, a TGG-based tool that leverages an incremental graph pattern matcher to handle model generation, batch transformation, incremental synchronisation, and consistency checking (with and without correspondence links) by applying essentially the same approach.

Short Papers

A Bidirectional Krivine Evaluator

Mikaël Mayer (University of Chicago) and Ravi Chugh (University of Chicago)

Bidirectional evaluation (Mayer et al., 2018) allows the output value of a lambda-term to be modified and then back-propagated through the term, repairing leaf terms as necessary. To accompany their call-by-value formulation, we present two call-by-name systems. First, we recount the call-by-value approach proposed by Mayer et al.; the key idea concerns back-propagating values through function application. Next, we formulate an analogous call-by-name system and establish corresponding correctness properties. Lastly, we define a backward Krivine-style evaluator that, while functionally equivalent to the “direct” by-name backward evaluator, exhibits notable characteristics.

Consistent Runtime Adaptation of User Interfaces

Anthony Anjorin (Paderborn University), Enes Yigitbas (Paderborn University), and Hermann Kaindl (TU Wien)

Modern User Interfaces (UIs) are increasingly expected to be plastic, in the sense that they retain a constant level of usability, even when subjected to context (platform, user, and environment) changes at runtime. Plasticity is often achieved by specifying suitable runtime adaptations of the UI as a response to changing contexts.

While there exist numerous approaches to enabling dynamic UI adaptation at runtime, we argue that a series of consistency-related challenges arise during the adaptation process, which have not yet been adequately addressed.

In this paper, therefore, we suggest a useful definition of consistency in this context, identify some important and open consistency-related challenges, and highlight solution strategies inspired by results and insights from research on bidirectional transformations.

Symmetric c-Lenses and Symmetric d-Lenses are Not Coextensive

Michael Johnson (Macquarie University) and François Renaud (Université Catholique de Louvain)

This short paper addresses a long standing open question about symmetric lenses, with the result succinctly summarised by the paper’s title. A more detailed description of the question is as follows. It has been clear for some years that symmetric lenses of various kinds can be constructed in a systematic way as equivalence classes of spans of asymmetric lenses of corresponding kinds. For example, given a definition of asymmetric delta lens, referred to here and elsewhere as a d-lens, one can systematically construct a notion of symmetric d-lens, and a category whose morphisms are those symmetric d-lenses. Among the d-lenses there are some particularly useful lenses, called c-lenses (and previously known to the mathematical community as split opfibrations) which have an attractive universal property that in many applications corresponds to least change updating. Naturally there has been interest in symmetric c-lenses, which can again by systematically constructed, and which might be expected to have an attractive universal property which could perhaps in applications capture a new notion of least change symmetric lens updating. However, the effects of the universal properties of the component c-lenses of a span of c-lenses occur mainly in the peak of the span, and that corresponds in applications to hidden data. Indeed, it can be shown that every span of c-lenses, viewed as a symmetric lens, is equivalent to a span of d-lenses in which the component d-lenses are not themselves c-lenses. In other words, the behaviour of a symmetric c-lens can always be obtained from a span of lenses which themselves do not have the c-lens universal property. And that raises the until now open question of whether there are in fact any differences at all between symmetric c-lenses and symmetric d-lenses. In this paper we show that a span of c-lenses does have a weak symmetric lens universal property, and that there are spans of d-lenses that do not exhibit this property, establishing that there are symmetric d-lenses which never arise as symmetric c-lenses.

Talks

A Toolbox of Lenses: Dimensions of the Lens Design Space

Zinovy Diskin (McMaster University)

Mathematical models are tools, and for their effective use, they should be placed in a properly organized toolbox and supplied with understandable prescriptions of “what tool is to be used for what purpose”. An accurate match can be especially important for lenses as a) they are tools for understanding and managing such a complex domain as synchronization, where mismatches can be especially painful, and b) the pool of lens structures existing today is big and diverse. The goal of the talk is to discuss how the lens tool space should be extended even more to better adapt it for practical applications, and how to organize it for better use. The talk will mainly be based on the ideas of paper [*] but will also broaden them.

[*] Zinovy Diskin, Harald König, Mark Lawford, Tom Maibaum: Toward Product Lines of Mathematical Models for Software Model Management. STAF Workshops 2017: 200-216

Expanding the Power of Lens Synthesis

Anders Miltner (Princeton University), Solomon Maina (University of Pennsylvania), Kathleen Fisher (Tufts University), Benjamin Pierce (University of Pennsylvania), David Walker (Princeton University), and Steve Zdancewic (University of Pennsylvania)

Recent work has shown how to synthesize a class of string bijections from regular expression specifications. These bijective string transformations can be useful for synchronizing simple data formats, but many interesting formats require non-bijective lenses. In this talk, we show how to expand the class of synthesized transformations beyond bijections to quotient lenses and a large subset of full symmetric lenses (including all the standard asymmetric lenses) through lightweight user annotations that help identify a “bijective core.”

Optics and Type Equivalences

Jacques Carette (McMaster University) and Amr Sabry (Indiana University Bloomington)

Bidirectional programming, lenses, prisms, and other optics have connections to reversible programming which have been explored from several perspectives, mostly by attempting to recover bidirectional transformations from unidirectional ones. We offer a novel and foundational perspective in which reversible programming is expressed using “type equivalences.” This perspective offers several advantages: first, it is possible to construct sets of sound and complete type equivalences for certain collections of types; these correspond to canonical optic constructions. Second, using ideas inspired by category theory and homotopy type theory, it is possible to construct sound and complete “equivalences between equivalences” which provide the canonical laws for reasoning about lens and prism equivalences.

Reified Correspondences: A New Component of the Multiary Delta Lenses Framework

Zinovy Diskin (McMaster University)

The talk motivates the necessity to modify the symmetric delta lens framework by including into it updates between intermodel correspondences (corrs). We will consider the setting in which an update propagation mechanism is defined over an alignment framework—this will allow us to separate simple (almost trivial) realignment and complex (far non-trivial) consistency restoration, and formalize Hippocraticness. Corr updates then appear in both realignment and consistency restoration, and make the mathematical framework much better aligned with the practice of model synchronization. The talk will provide precise definitions, and sketch possible directions for the development of the framework.

Unless otherwise stated, the content of this page is licensed under GNU Free Documentation License.