## Spring Festival Workshop on Programming Languages

### General information

Time | 10:00–18:30, Friday 20 February 2015 (followed by a post-workshop dinner) |
---|---|

Place | Rooms 1901–1903 (19th floor), National Institute of Informatics, Japan 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo 101-8430 （〒101-8430 東京都千代田区一ツ橋 2-1-2）[Google Maps] |

Contact | Josh Ko, hsiang-shang [at] nii [dot] ac [dot] jp |

### Post-workshop dinner

Location | Sakura Jimbochoten （咲くら 神保町店） |
---|---|

Address | Iwanami Jimbocho building B1, 2-1 Kandajinbocho, Chiyoda-ku, Tokyo 101-0051 （〒101-0051 東京都千代田区神田神保町 2-1 岩波神保町ビル B1）[Google Maps] |

Website | https://gurunavi.com/en/g851544/rst |

Price | about 5,000JPY (2,000JPY for students) |

If you wish to attend the dinner, please let us know by noon on the day of the workshop. |

### Invited talks

Notions of Bidirectional Computation and Entangled State Monads

Jeremy Gibbons (University of Oxford, UK)

Bidirectional transformations (bx) support principled consistency maintenance among data sources. Each data source corresponds to one perspective on a composite system, manifested by operations to “get” and “put” a view of the whole from that perspective. Bx are important in a wide range of settings, including databases, interactive applications, and model-driven development. We show that bx are naturally modelled in terms of mutable state; in particular, the “put” operations are stateful functions. This leads naturally to considering bx that exploit other computational effects too, such as I/O, nondeterminism, and failure, which have largely been ignored in the bx literature to date. We present a semantic foundation for symmetric bidirectional transformations with effects. We build on the mature theory of monadic encapsulation of effects in functional programming, develop the equational theory and important combinators, and provide a prototype implementation in Haskell along with several illustrative examples.

This is joint work with Faris Abou-Saleh, James Cheney, James McKinna, and Perdita Stevens.

[slides]

Embedding Attribute Grammars and Their Extensions with Functional Zippers

João Saraiva (University of Minho, Portugal)

Attribute grammars are a suitable formalism to express complex software language analysis and manipulation algorithms, which rely on multiple traversals of the underlying abstract tree. Attribute Grammars have been extended with mechanisms such as references and high-order and circular attributes. Such extensions provide a powerful modular mechanism and allow the specification of (tree and graph-based) complex computations. In this talk we present an elegant and simple, zipper-based embedding of attribute grammars and their extensions as first class citizens. In this setting, language specifications are defined as a set of independent, off-the-shelf components that can easily be composed into a powerful, executable language specification. Incremental attribute evaluation are used to avoid re-calculation of attributes and some benchmarks results will be presented.

[slides]

### Contributed talks

Bidirectional Transformation on Ordered Graphs

Soichiro Hidaka (National Institute of Informatics, Japan)

The language-based approach plays an important role in the development of well-behaved structural bidirectional transformations. It has been successfully applied to solve the challenging problem of bidirectional transformation on graphs by establishing a clear bidirectional semantics based on a bulk semantics of the structural recursion. However, this result was limited to unordered graphs, where the order between outgoing edges of nodes is disregarded, and it was not clear how to treat ordered ones such as XML documents with pointers. lambdaFG is a language for querying ordered graphs, in which, a bulk semantics of structural recursion, extend with children rearrangement capability, is provided in a unidirectional setting. In this presentation, we show that (the first-order subset of) lambdaFG can be bidirectionalized by a three-stage procedure. The forward evaluation generates a view graph with comprehensive order-aware trace information. The traceable view enables us to reflect the edits on the view to the updates in the source by backward evaluation. We adopt a classical notion of epsilon-edges to represent the unobservable short cuts between nodes, which are fully utilized in bidirectionalization to keep the original shape of the input graphs. Thus our bidirectionalization is completed by a novel order-aware bidirectional procedure to eliminate epsilon-edges. This is a joint work with Fei Yang.

[slides]

Escaping from the Haskell Library Dependency Hell: Scalable component programming in current Haskell

Oleg Kiselyov (Tohoku University, Japan)

Modularity is one of the key principles of software engineering, dictating a software system be assembled from separately developed and tested, and easily interchangeable and extensible parts with clear interface. We call such parts, which provide a set of related data types and operations on them, components. Component programming — assembling components and writing them (often by assembling or extending other components) — particularly proves its worth during the evolution of large code bases.

At first blush, component programming in Haskell seems impossible. Although Haskell has separately-compiled modules, it does not separate module interface and implementation and has no notion of module types. To refer to operations in other Haskell modules, we have to import them by the name of the implementation file rather than by the interface. Therefore, extending one module sets off the cascade of recompilation. Using two versions of a component in the same project requires maintaining two separate, although mostly identical, code bases. The hard-wiring of module names is responsible for numerous versioning problems, the unremitting bane of Haskell installations.

Although Haskell modules are not extensible components, scalable component programming is nevertheless possible, as we demonstrate on two case studies. We show how to use type classes as interfaces (component signatures) and how to systematically replace hard links — references to components and their types and values by name — with references by interfaces. The approach is compelling in sufficiently complex cases, especially mutually dependent extensible components; otherwise, ordinary closures suffice.

Generating attribute grammar-based bidirectional transformations from rewrite rules

Pedro Martins (University of Minho, Portugal)

Higher order attribute grammars provide a convenient means for specifying unidirectional transformations, but they provide no direct support for bidirectional transformations. In this paper we show how rewrite rules (with non-linear right hand sides) that specify a forward/get transformation can be inverted to specify a partial backward/put transformation. These inverted rewrite rules can then be extended with additional rules based on characteristics of the source language grammar and forward transformations to create, under certain circumstances, a total backward transformation. Finally, these rules are used to generate attribute grammar specifications implementing both transformations.

[slides]

Attribute-Based Access Control Models

Lionel Montrieux (National Institute of Informatics, Japan)

Computer access control has a long history, which started with the first multi-user systems. The purpose of access control is to restrict access to resources to only certain subjects, under certain circumstances. One current area of research in access control is Attribute-Based Access Control (ABAC) models. ABAC models are authorisation models where attributes are attached to subjects, resources, actions or the environment, and the values of those attributes are used to decide whether a request for access to a resource should be granted or denied. This talk will explore the ABAC models that have been proposed by the research community, as well as those that are used in industrial settings.

[slides]

BiFluX: Put-based bidirectional transformations for XML document synchronisation (demo)

Josh Ko (National Institute of Informatics, Japan) and Zirun Zhu (SOKENDAI — The Graduate University of Advanced Studies, Japan)

We give a brief introduction to the idea of put-based bidirectional
transformations and demonstrate a put-based XML document synchronisation
tool *BiFluX*, featuring a high-level SQL-like language for
writing put transformations, from which unique get transformations
are automatically derived.

[slides]

Implementing Type Inference in Agda

Kenichi Asai (Ochanomizu University, Japan)

In dependently-typed languages like Agda, a type checking problem is often formulated nicely as a transformation of a raw term into either a well-typed term (when the input is well-typed) or a reason why it is not well-typed. However, it assumes that all the bound variables are annotated with their types. In this talk, I describe how to write the type inference problem, rather than the type checking problem, in Agda. Without type annotations, we have to assign type variables to bound variables and perform unification on types. To ensure termination, we use McBride's unification algorithm and carefully keep track of the number of type variables during type inference.

[slides]

Hiroyuki Kato (National Institute of Informatics, Japan)

XQuery is widely used in practice including data integration in DB community, semantic web in AI community, document and the Web data processing in industry and so on. However, a side-effect in XQuery is a barrier to query optimization based on a static analysis. In this talk, I will talk about our ongoing work on XQuery fusion in which any XQuery expressions in practical usage can be transformed into ones in a treeless form.

[slides]

Principles of Reversible Computation

Robert Glück (University of Copenhagen, Denmark)

Reversible computation — the study of computing models deterministic in both the forward and backward directions — has a growing number of application areas such as program debugging and testing, modeling, programming language and low-energy hardware design. In this talk we present the principles of a reversible abstract machine and its programming language. For a programmable computing system to be reversible, both the underlying control logic and each instruction must be reversible. Joint work with Holger Bock Axelsen, Stéphane Burignat, Alex De Vos, Michael Thomsen and Tetsuo Yokoyama (U Copenhagen, U Ghent, U Nanzan).

[handout]

**Related References**

- Axelsen H.B., Glück R., De Vos A., Thomsen M.K., MicroPower: towards low-power microprocessors with reversible computing. ERCIM News, Special Theme: Towards Green ICT, 79(1): 20–21, 2009.
- Axelsen H.B., Glück R., What do reversible programs compute? Hofmann M. (ed.), Foundations of Software Science and Computation Structures. Proceedings. LNCS 6604, 42–56, 2011.
- Glück R., Yokoyama T. (eds.), Reversible Computation. Proceedings. Lecture Notes in Computer Science. Vol. 7581, 2013.
- Axelsen H.B., Glück R., Yokoyama T., Reversible machine code and its abstract processor architecture. Diekert V., et al. (eds.), Computer Science — Theory and Applications. Proceedings. LNCS 4649, 56–69, 2007.
- Thomsen M.K., Glück R., Axelsen H.B., Reversible arithmetic logic unit for quantum arithmetic. Journal of Physics A: Mathematical and Theoretical, 43(38): 382002, 2010.