View: session overviewtalk overviewside by side with other conferences
11:00 | 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. |
11:30 | 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. |
12:00 | 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. |
Lunches will be held in Taub hall and in The Grand Water Research Institute.
14:00 | 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. |
14:30 | 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. |
15:00 | 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. |
16:00 | PRESENTER: Vlad Rusu 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. |
16:30 | Towards a Refactoring Tool for Dependently-Typed Programs (work in progress) PRESENTER: Christopher Brown 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. |
16:45 | 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. |