FLOPS 2020: 15TH INTERNATIONAL SYMPOSIUM ON FUNCTIONAL AND LOGIC PROGRAMMING
PROGRAM FOR WEDNESDAY, SEPTEMBER 16TH
Days:
previous day
all days

View: session overviewtalk overview

20:00-21:30 Session 5
Chair:
Konstantinos Sagonas (Uppsala University, Sweden)
20:00
Kanae Tsushima (National Institute of Informatics, Japan)
Bách Nguyễn Trọng (National Institute of Informatics, Japan)
Robert Glück (University of Copenhagen, Denmark)
Zhenjiang Hu (Peking University, China)
An efficient composition of bidirectional programs by memoization and lazy update

ABSTRACT. Bidirectional transformations (BX) are a solution to the view update problem and widely used for synchronizing data. The semantics and correctness of bidirectional programs have been investigated intensively during the past years, but their efficiency and optimization are not yet fully understood. In this paper, as a first step, we study different evaluation methods to optimize their evaluation. We focus on the interpretive evaluation of BX compositions because we found that these compositions are an important cause of redundant computations if the compositions are not right associative. For evaluating BX compositions efficiently, we investigate two memoization methods. The first method, minBiGUL$_m$, uses memoization, which improves the runtime of many BX programs by keeping intermediate results for later reuse. A disadvantage is the familiar tradeoff for keeping and searching values in a table. When inputs become large, the overhead increases and the effectiveness decreases. To deal with large inputs, we introduce the second method, $xpg$, that uses tupling, lazy update and lazy evaluation as optimizations. Lazy updates delay updates in closures and enables to use them later. Both evaluation methods were fully implemented for minBiGUL. The experimental results show that our methods are faster than the original method of BiGUL for the non-right associative compositions.

20:30
Rui Okura (University of Tsukuba, Japan)
Yukiyoshi Kameyama (University of Tsukuba, Japan)
Language-Integrated Query with Nested Data Structures and Grouping
PRESENTER: Rui Okura

ABSTRACT. Language-integrated query adds to database query the power of high-level programming languages such as abstraction, compositionality, and nested data structures. Cheney et al. designed a two-level typed language for it and showed that any term of suitable type can be normalized to a single SQL query (normalization property for short).

This paper extends their language to cover a simple form of grouping and aggregate functions. Although they are frequently used primitives in SQL, they are not covered by existing studies on efficient implementation of language-integrated query. One of the reasons is that grouping in SQL not only does grouping and aggregation, but also composes complicated outputs; the former cannot be normalized but has no nested data structures, while the latter is opposite.

To solve this problem, we introduce aggregate functions with grouping to their language. They are simpler than SQL's grouping primitive in that it can return only the results of aggregate functions. By decoupling grouping-and-aggregation and output-composition, we get a simple calculus, while keeping the normalization property. We conduct simple benchmarks which show that queries in our language can be transformed to efficient SQL queries.

21:00
Oliver Westphal (University of Duisburg-Essen, Germany)
Janis Voigtländer (University of Duisburg-Essen, Germany)
Implementing, and keeping in check, a DSL used in e-learning
PRESENTER: Oliver Westphal

ABSTRACT. We discuss a DSL intended for use in an education setting, when teaching the writing of interactive Haskell programs to students. The DSL was previously presented as a small, formal language of specifications capturing the behavior of simple console I/O programs, along with a trace-based semantics. A prototypical implementation also exists. When going for productive application in an actual course setting, several robustness and usability questions arise. For example, if programs written by students are mechanically checked and graded by the implementation, what guarantees are there for the educator that the assessment is correct? Does the implementation really agree with the on-paper semantics? What else can inform the educator's writing of a DSL expression when developing a new exercise task? Which activities beyond testing of student submissions can be mechanized based on the specification language, for example concerning material handed to students in support of task understanding, before, and feedback or trusted sample solutions, after their own solution attempts? Also, how to keep the framework maintainable, preserving its guarantees when the expressiveness of the underlying DSL is to be extended? Our aim here is to address these and related questions, reporting on connections we have made and concrete steps we have taken, as well as the bigger picture.

22:00-23:15 Session 6
Chair:
Zhenjiang Hu (Peking University, China)
22:00
Matteo Cimini (University of Massachusetts Lowell, United States)
On the Effectiveness of Higher-Order Logic Programming in Language-Oriented Programming

ABSTRACT. Lang-n-play is a functional language-oriented programming language with languages as first-class-citizens. Language definitions can be bound to variables, passed to and returned by functions, and can be modified at run-time before being used. Lang-n-play programs are compiled and executed in the high-order logic programming language Lambda-Prolog. In this paper, we describe our compilation method, which highlights how the distinctive features of high-order logic programming are a great fit in implementing languages a language-oriented programming language.

22:30
Benjamin Mourad (University of Massachusetts Lowell, United States)
Matteo Cimini (University of Massachusetts Lowell, United States)
System Description: Lang-n-Change -- A Tool for Transforming Languages
PRESENTER: Benjamin Mourad

ABSTRACT. Lang-n-Change is a tool for transforming language defintions into other language definitions. It provides a declarative domain-specific language for expressing algorithms over languages. Lang-n-Change is implemented in OCaml and generates language definitions that can be compiled and executed in Lambda-Prolog.

23:00
Sophie Fortz (University of Namur, Belgium)
Fred Mesnard (université de la Réunion, France)
Etienne Payet (LIM, Université de La Réunion, Reunion)
Gilles Perrouin (University of Namur, Belgium)
Wim Vanhoof (University of Namur, Belgium)
German Vidal (MiST, VRAIN, Universitat Politecnica de Valencia, Spain)
An SMT-Based Concolic Testing Tool for Logic Programs (System Description)
PRESENTER: Sophie Fortz

ABSTRACT. Concolic testing mixes symbolic and concrete execution to generate test cases covering paths effectively. Its benefits have been demonstrated for more than 15 years to test imperative programs. Other programming paradigms, like logic programming, have received less attention. In this paper, we present a concolic-based test generation method for logic programs. Our approach exploits SMT-solving for constraint resolution. We also describe the implementation of a concolic testing tool for Prolog.

23:15-23:30 Closing
Chair:
Keisuke Nakano (Tohoku University, Japan)