View: session overviewtalk overviewside by side with other conferences

08:30-09:00Coffee & Refreshments
09:30-10:30 Session 3B: Invited Talk
Location: Ullmann 305
Transforming Text to (and from) XML

ABSTRACT. In industry, there is a critical need for complying with laws, standards, and guidelines. However, there are hundreds of (versions of) international and regional standards and guidelines, and each of them has hundreds of clauses, referring to each other. In AIST, we are developing an XML-based framework to support human developers to navigate the vast amount of documents.

In this talk, I will introduce a Text-to-XML structuring tool TXtruct, a core ingredient of the aforementioned framework.

TXtruct is a language that can describe a text or XML grammar, and at the same time can describe a transformer. Despite the strength, the TXtruct interpreter is implemented in an elegant and minimalistic way, based on a string-diagrammatic semantics. We will discuss some important properties such as termination, productivity, and invertibility.

We will also explore the potential applications in the Termination Competitions and Confluence Competitions, where thousands of term rewrite systems are given in a different formats.

10:30-11:00Coffee Break
11:00-12:30 Session 10M: Talks (1)
Location: Ullmann 305
Program Equivalence in a Typed Probabilistic Call-by-Need Functional Language
PRESENTER: David Sabel

ABSTRACT. We introduce a call-by-need variant of PCF with a binary probabilistic fair choice operator. We define its operational semantics and contextual equivalence as program equivalence, where the expected convergence is only observed on numbers. We investigate another program equivalence that views two closed expressions as distribution-equivalent if evaluation generates the same distribution on the natural numbers. We show that contextual equivalence implies distribution-equivalence. Future work is to provide a full proof of the opposite direction.

A Machine-Checked Formalisation of Erlang Modules
PRESENTER: Péter Bereczky

ABSTRACT. This paper contributes to our long-term goal of defining the Erlang programming language in the Coq proof assistant, ultimately allowing us to formally reason about Erlang programs and their transformations. In previous work, we have described a sequential subset of the core language of Erlang in different semantics definition styles, which is extended with the module system in the present formalization. In particular, we define modules and inter-module calls in natural and functional big-step semantics, and we prove their equivalence. Last but not least, we validate the formal definition with respect to the reference implementation. The formal theories are machine-checked in Coq.

Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems
PRESENTER: Kasper Hagens

ABSTRACT. When transforming a program into a more efficient version (for example translating a recursive program into an imperative program), it is important to guarantee that the input-output-behavior remains the same. One approach to assure this uses so-called Logically Constrained Term Rewriting Systems (LCTRSs). Two versions of a program are translated into LCTRSs and compared in a proof system (Rewriting Induction). Proving their equivalence in this system often requires the introduction of a lemma. In this paper we review a lemma generation approach by Fuhs, Kop and Nishida and propose two possible extensions.

12:30-14:00Lunch Break

Lunches will be held in Taub hall and in The Grand Water Research Institute.

14:00-15:30 Session 14P: Talks (2)
Location: Ullmann 305
On Reducing Non-Occurrence of Specified Runtime Errors to All-Path Reachability Problems of Constrained Rewriting
PRESENTER: Naoki Nishida

ABSTRACT. A concurrent program with semaphore-based exclusive control can be transformed into a logically constrained term rewrite system that is computationally equivalent to the program. In this paper, we first propose a framework to reduce the non-occurrence of a specified runtime error in the program to an all-path reachability problem of the transformed logically constrained term rewrite system. Here, an all-path reachability problem is a pair of state sets and is demonically valid if every finite execution path starting with a state in the first set and ending with a terminating state includes a state in the second set. Then, as a case study, we show how to apply the framework to the race-freeness of semaphore-based exclusive control in the program. Finally, we show a simplified variant of a proof system for all-path reachability problems.

On Transforming Rewriting-Induction Proofs for Logical-Connective-Free Sequents into Cyclic Proofs
PRESENTER: Shujun Zhang

ABSTRACT. A GSC-terminating and orthogonal inductive definition set (IDS, for short) of first-order predicate logic can be transformed into a many-sorted term rewrite system (TRS, for short) such that a quantifier-free sequent is valid w.r.t. the IDS if and only if a term equation representing the sequent is an inductive theorem of the TRS. Under certain assumptions, it has been shown that a quantifier- and cut-free cyclic proof of a sequent can be transformed into a rewriting-induction (RI, for short) proof of the corresponding term equation. The RI proof can be transformed back into the cyclic proof, but it is not known how to transform arbitrary RI proofs into cyclic proofs. In this paper, we show that for a quantifier- and logical-connective-free sequent, if there exists an RI proof of the corresponding term equation, then there exists a cyclic proof of some sequent w.r.t. some IDS such that the cyclic proof ensures the validity of the initial sequent. To this end, we show a transformation of the RI proof into such a cyclic proof, a sequent, and an IDS.

On Transforming Imperative Programs into Logically Constrained Term Rewrite Systems via Injective Functions from Configurations to Terms
PRESENTER: Naoki Nishida

ABSTRACT. To transform an imperative program into a logically constrained term rewrite system (LCTRS, for short), previous work converts a statement list to rewrite rules in a stepwise manner, and proves the correctness along such a conversion and the big-step semantics of the program. On the other hand, the small-step semantics of a programming language comprises of inference rules that define transition steps of configurations. Partial instances of such inference rules are almost the same as rewrite rules in the transformed LCTRS. In this paper, we aim at establishing a framework for plain definitions and correctness proofs of transformations from programs into LCTRSs. To this end, for the transformation in previous work, we show an injective function from configurations to terms, and reformulate the transformation by means of the injective function. The injective function maps a transition step to a reduction step, and results in a plain correctness proof.

15:30-16:00Coffee Break
16:00-17:30 Session 19M: Talks (3)
Location: Ullmann 305
Towards Corecursion Without Corecursion in Coq

ABSTRACT. Coinduction is an important concept in functional programming. To formally prove properties of corecursive functions one can try to define them in a proof assistant such as Coq. But there arelimitations on the  functions that can be defined. In particular, corecursive calls must occur directly under a call to a constructor, without any  calls to other recursive functions in between. In this paper we show how a partially ordered set endowed with a notion of approximation can be organized as a Complete Partial Order. This makes it possible to define corecursive functions without using Coq's corecursion,  as the unique solution of a fixpoint equation, thereby escaping Coq's builtin limitations.

Towards a Refactoring Tool for Dependently-Typed Programs (work in progress)

ABSTRACT. While there is considerable work on refactoring functional programs, so far this had not extended to dependently-typed programs. In this paper, we begin to explore this space by looking at a range of transformations related to indexed data and functions.

Refactoring Steps for P4 (work in progress)
PRESENTER: Máté Tejfel

ABSTRACT. P4 is a domain specific programming language developed mainly to describe data plane layer of packet processing algorithms of different network devices (e.g. switches, routers). The language has special domain-specific constructs (e.g. match/action tables) that cannot be found in other languages and as such there is no existing methodology yet for refactoring these constructs. The paper introduces the definition of some P4 specific refactoring steps. The proposed steps are implemented using P4Query an analyzer framework dedicated to P4.