Spring Festival Workshop 2017 @ Karuizawa!

General information

21 ~ 23, March, 2017
Josh Ko, hsiang-shang [at] nii [dot] ac [dot] jp
We usually take Shinkansen to Karuizawa JR Station,
and then take a 30-minute walk to the Seminar House


18:30 on 21 March


An Axiomatic Basis for Bidirectional Programming

Hsiang-Shang Ko (National Institute of Informatics, Japan)

Among the frameworks of bidirectional transformations proposed for addressing various synchronisation problems, Foster et al.’s asymmetric lenses have influenced the design of a generation of bidirectional programming languages. Most of these languages are highly declarative, and only allow the programmer to specify a consistency relation with limited control over the behaviour of the automatically derived consistency restorer. However, synchronisation problems are diverse and require vastly different consistency restoration strategies, and the programmer must be empowered to fully control and reason about the consistency restoration behaviour of their bidirectional programs. The putback-based approach to bidirectional programming was proposed to address this issue once and for all, and this talk will present the latest result along this line of research: a Hoare-style logic for the putback-based language BiGUL. With this Hoare-style logic, the BiGUL programmer can precisely characterise the bidirectional behaviour of their programs by reasoning solely in the putback direction. The theory underlying the Hoare-style logic has been formalised and checked in the dependently typed language Agda, but this talk will give a semi-formal presentation of the logic suitable for human reasoning.

This is joint work with Zhenjiang Hu.


Unification of Parsing and Reflective Printing

Zirun Zhu (National Institute of Informatics, Japan)

Parsers and printers (or unparsers, serialisers) are needed as the frontend of a compiler for programming languages. Despite the fact that they are doing conversion in opposite direction and being closely related, the mainstream practice is to design the two components independently, at a high risk of failing to preserve consistencies between the two. For example, if we parse the program text printed from an abstract syntax tree (AST), we want to get an identical AST as before (1); or if we print an AST previously parsed from a piece of program text, the newly produced program text is supposed to be identical to the original one — it had better also include all the comments and layouts detail (2) . Keeping the two properties is useful in various situations, such as producing error messages, observing evaluation process in terms of surface syntax, reflect changes done by code refactor algorithms back to program text, etc.

A natural idea is to have a small but declarative domain specific language (DSL) to help the user program consistent parsers and printers easily. Indeed, these demands had driven us to invent BiYacc (a DSL). The two natural observations (1) and (2) seem easy to keep and straightforward for implementation. This is true, however, only in the absence of grammar ambiguity and syntactic sugar. So in the second half of the talk, we will discuss how the ambiguity and syntactic sugar cause additional difficulties. We present our current solution, in which we adopt the asymmetric lens bidirectional transformation framework, and the two natural observations are summarised as GetPut and PutGet laws. Furthermore, we will discuss how to produce ``better'' program text when the given program text does not naively match the given AST by position.


HOBiT: a Higher-Order Bidirectional Programming Language

Kazutaka Matsuda (Tohoku University, Japan)

A bidirectional transformation is a pair of mappings between source and view data objects, one in each direction. When the view is modified, the source is updated accordingly with respect to some laws---a pattern that is very common in databases, model-driven development, compiler construction, and so on. As a result, there has been a number of languages designed for programming with bidirectional transformations. Despite this effort, the practicality of bidirectional languages remains an open problem. Existing languages either force programmers to a non-conventional programming style, denying them many of the established abstraction methods, or restrict the set of possible data that can be transformed, or both, leaving programmers little choice in *what* and *how* programs can be written.

To address this issue, we propose a higher-order bidirectional programming language HOBiT. The language advances the state of the art in a number ways. It supports higher-order programming in the applicative style---one can freely use the conventional functional programming mechanisms of lambda abstraction and pattern matching. And at the same time, the language allows refined control of program behaviours in both directions through a construct known as bidirectional case analysis, resulting in robust bidirectional transformations that handle a wide range of data changes. This is joint work with Meng Wang.


Profunctor Optics: Modular Data Accessors

Jeremy Gibbons (University of Oxford, UK)

Data accessors allow one to read and write components of a data structure; examples include lenses for accessing the fields of a record, prisms for accessing the variants of a union, and traversals for accessing the elements of a container. These data accessors are collectively known as optics; they are fundamental to programs that manipulate complex data. Individual data accessors for simple data structures are easy to write, for example as pairs of "getter" and "setter" methods. However, it is not obvious how to combine data accessors, in such a way that data accessors for a compound data structure are composed out of smaller data accessors for the parts of that structure. Generally, one has to write a sequence of statements or declarations that navigate step by step through the data structure, accessing one level at a time - which is to say, data accessors are traditionally not first-class citizens, combinable in their own right. We present a framework for modular data access, in which individual data accessors for simple data structures may be freely combined to obtain more complex data accessors for compound data structures. Data accessors become first-class citizens. The framework is based around the notion of profunctors, a flexible generalization of functions. (This is joint work with Matthew Pickering and Nicolas Wu.)


Palgol: A High-Level DSL for Vertex-Centric Graph Processing with Remote Data Access

Yongzhe Zhang (National Institute of Informatics, Japan)

Pregel is a popular parallel computing model for dealing with large-scale graphs. However, it can be tricky to implement graph algorithms correctly and efficiently in Pregel’s vertex-centric model, as programmers need to carefully restructure an algorithm in terms of supersteps and message passing, which are low-level and detached from the algorithm descriptions. Some domain-specific languages (DSLs) have been proposed to provide more intuitive ways to implement graph algorithms, but none of them can flexibly describe remote access (reading or writing attributes of other vertices through references), causing a still wide range of algorithms hard to implement.

To address this problem, we design and implement Palgol, a more declarative and powerful DSL which supports remote access. In particular, programmers can use a more declarative syntax called global field access to directly read data on remote vertices. By structuring supersteps in a high-level vertex-centric computation model and analyzing the logic patterns of global field access, we provide a novel algorithm for compiling Palgol programs to efficient Pregel code. We demonstrate the power of Palgol by using it to implement a bunch of practical Pregel algorithms and compare them with hand-written code. The evaluation result shows that the efficiency of Palgol is comparable with that of hand-written code. This is joint work with Hsiang-Shang Ko and Zhenjiang Hu.


CPS Translating Dependent Types

Youyou Cong (Ochanomizu University, Japan)

We present an implementation of a type-preserving CPS translation for the lambda calculus with dependent function types. Our meta language is Agda, a dependently typed functional programming language. We define the translation as a function from well-typed terms to well-typed terms, therefore the function itself can be understood as a proof of type preservation. This is joint work with Kenichi Asai.


Programming Derivatives: Towards Change-Oriented Programming

Zhenjiang Hu (National Institute of Informatics, Japan)

Change is essential and expensive in software development. Although a significant amount of work has been done on software change, its status as a scientific discipline is still an open challenge. In this talk, I will show that it is possible to treat software change as a first-class citizen, and that we can program changes through direct coding of derivatives.

Correctness Enhancement as a Pervasive Software Engineering Paradigm

Ali Mili (New Jersey Institute of Technology, US)

In the seventeenth century play by French author Moliere titled ''Le Bourgeois Gentilhomme'', the title character Monsieur Jourdain, upon learning that speech is divided into two categories, prose and verse, is thrilled to discover that he has been saying prose all his life but did not know it. In this talk, we argue that software engineers are overdue for a similar discovery: we have been doing correctness enhancement all our life and many (perhaps most) of us did not know it; where correctness enhancement is the process of making a program more-correct with respect to a specification. Indeed, we find that such diverse activities as program construction, corrective maintenance, adaptive maintenance, program repair, software merger, software upgrade, test-based development, feature-driven development, agile development, etc... are all instances of correctness enhancement. If we want this epiphany to do us more good than Monsieur Jourdain's did him, we need to achieve three goals: 1) Define correctness enhancement. 2) Model existing processes as instances of correctness enhancement. 3) Explore means to use the mathematics of correctness enhancement to advance the practice of these processes.

[pdf slides] [ppt slides]

Right Repetitive Application of Combinators

Keisuke Nakano (University of Electro-Communications, Japan)

B-terms are built from the B combinator alone defined by B f g x = f (g x), which is well-known as a function composition operator. In this talk, I introduce an interesting property of B-terms, that is, whether repetitive right applications of a B-term circulates or not. I will show the sufficient conditions for B-terms to and not to have the property through a canonical representation of B-terms and a sound and complete equational axiomatization. This is a partial solution to a conjecture which has been open since 2003.

Towards Derivation of Monadic Programs: A Case Study of States and Nondeterminism

Shin-Cheng Mu (Academia Sinica, Taiwan)

Equational reasoning is among the most important tools that functional programming provides us. Curiously, relatively little attention has been paid on reasoning about monadic programs. In this talk we propose some theorems and patterns useful for derivation of monadic programs, focusing on non-determinism and states.


A Type Error Debugger with Slicer (+ Patterns)

Kanae Tsushima (National Institute of Informatics, Japan)

Recently we implemented a type error slicer in OCaml. Thanks to it, the number of questions by our interactive type error debugger is reduced. In this talk, I'd like to talk about results by type error slicer and how can we treat patterns in our type error debugger and slicer.

An Experiment in Ping-Pong Protocol Verification by Pushdown Automata

Robert Glück (University of Copenhagen, Denmark)

We discuss an in-progress experiment to verify the security of ping-pong protocols (Dolev-Yao intruder model) using nondeterministic two-way pushdown automata (2NPDA). The pushdown automaton checks whether the intersection of a regular language (the protocol to verify) and a Dyck language containing all canceling words is empty. If the languages have a word in common, an intruder can reveal a secret message sent between trusted users. The verification takes at most cubic time on our 2NPDA-simulator, while the actual run of the checking 2NPDA takes exponential time. The experiment also explores the uses of nondeterministic programming for solving polynominal-time problems without the typical exponential-time penalty of such programs. This is an application of our memoizing pushdown-automata simulation [1].

Reference: [1] Glück R., A practical simulation result for two-way pushdown automata. In Han Y.-S., Salomaa K. (eds.), Implementation and Application of Automata. LNCS 9705, 2016. http://dx.doi.org/10.1007/978-3-319-40946-7_10