-
Extensional and Non-extensional Functions as Processes
Authors:
Ken Sakayori,
Davide Sangiorgi
Abstract:
Following Milner's seminal paper, the representation of functions as processes has received considerable attention. For pure $λ$-calculus, the process representations yield (at best) non-extensional $λ$-theories (i.e., $β$ rule holds, whereas $η$ does not).
In the paper, we study how to obtain extensional representations, and how to move between extensional and non-extensional representations. U…
▽ More
Following Milner's seminal paper, the representation of functions as processes has received considerable attention. For pure $λ$-calculus, the process representations yield (at best) non-extensional $λ$-theories (i.e., $β$ rule holds, whereas $η$ does not).
In the paper, we study how to obtain extensional representations, and how to move between extensional and non-extensional representations. Using Internal $π$, $\mathrm{I}π$ (a subset of the $π$-calculus in which all outputs are bound), we develop a refinement of Milner's original encoding of functions as processes that is parametric on certain abstract components called wires. These are, intuitively, processes whose task is to connect two end-point channels. We show that when a few algebraic properties of wires hold, the encoding yields a $λ$-theory. Exploiting the symmetries and dualities of $\mathrm{I}π$, we isolate three main classes of wires. The first two have a sequential behaviour and are dual of each other; the third has a parallel behaviour and is the dual of itself. We show the adoption of the parallel wires yields an extensional $λ$-theory; in fact, it yields an equality that coincides with that of Böhm trees with infinite $η$. In contrast, the other two classes of wires yield non-extensional $λ$-theories whose equalities are those of the Lévy-Longo and Böhm trees.
△ Less
Submitted 6 May, 2024;
originally announced May 2024.
-
Ownership Types for Verification of Programs with Pointer Arithmetic
Authors:
Izumi Tanaka,
Ken Sakayori,
Naoki Kobayashi
Abstract:
Toman et al. have proposed a type system for automatic verification of low-level programs, which combines ownership types and refinement types to enable strong updates of refinement types in the presence of pointer aliases. We extend their type system to support pointer arithmetic, and prove its soundness. Based on the proposed type system, we have implemented a prototype tool for automated verifi…
▽ More
Toman et al. have proposed a type system for automatic verification of low-level programs, which combines ownership types and refinement types to enable strong updates of refinement types in the presence of pointer aliases. We extend their type system to support pointer arithmetic, and prove its soundness. Based on the proposed type system, we have implemented a prototype tool for automated verification of the lack of assertion errors of low-level programs with pointer arithmetic, and confirmed its effectiveness through experiments.
△ Less
Submitted 11 December, 2023;
originally announced December 2023.
-
Borrowable Fractional Ownership Types for Verification
Authors:
Takashi Nakayama,
Yusuke Matsushita,
Ken Sakayori,
Ryosuke Sato,
Naoki Kobayashi
Abstract:
Automated verification of functional correctness of imperative programs with references (a.k.a. pointers) is challenging because of reference aliasing. Ownership types have recently been applied to address this issue, but the existing approaches were limited in that they are effective only for a class of programs whose reference usage follows a certain style. To relax the limitation, we combine th…
▽ More
Automated verification of functional correctness of imperative programs with references (a.k.a. pointers) is challenging because of reference aliasing. Ownership types have recently been applied to address this issue, but the existing approaches were limited in that they are effective only for a class of programs whose reference usage follows a certain style. To relax the limitation, we combine the approaches of ConSORT (based on fractional ownership) and RustHorn (based on borrowable ownership), two recent approaches to automated program verification based on ownership types, and propose the notion of borrowable fractional ownership types. We formalize a new type system based on the borrowable fractional ownership types and show how we can use it to automatically reduce the program verification problem for imperative programs with references to that for functional programs without references. We also show the soundness of our type system and the translation, and conduct experiments to confirm the effectiveness of our approach.
△ Less
Submitted 31 October, 2023;
originally announced October 2023.
-
Termination Analysis for the $π$-Calculus by Reduction to Sequential Program Termination
Authors:
Tsubasa Shoshi,
Takuma Ishikawa,
Naoki Kobayashi,
Ken Sakayori,
Ryosuke Sato,
Takeshi Tsukada
Abstract:
We propose an automated method for proving termination of $π$-calculus processes, based on a reduction to termination of sequential programs: we translate a $π$-calculus process to a sequential program, so that the termination of the latter implies that of the former. We can then use an off-the-shelf termination verification tool to check termination of the sequential program. Our approach has bee…
▽ More
We propose an automated method for proving termination of $π$-calculus processes, based on a reduction to termination of sequential programs: we translate a $π$-calculus process to a sequential program, so that the termination of the latter implies that of the former. We can then use an off-the-shelf termination verification tool to check termination of the sequential program. Our approach has been partially inspired by Deng and Sangiorgi's termination analysis for the $π$-calculus, and checks that there is no infinite chain of communications on replicated input channels, by converting such a chain of communications to a chain of recursive function calls in the target sequential program. We have implemented an automated tool based on the proposed method and confirmed its effectiveness.
△ Less
Submitted 1 September, 2021;
originally announced September 2021.
-
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving
Authors:
Takumi Shimoda,
Naoki Kobayashi,
Ken Sakayori,
Ryosuke Sato
Abstract:
Despite the recent advance of automated program verification, reasoning about recursive data structures remains as a challenge for verification tools and their backends such as SMT and CHC solvers. To address the challenge, we introduce the notion of symbolic automatic relations (SARs), which combines symbolic automata and automatic relations, and inherits their good properties such as the closure…
▽ More
Despite the recent advance of automated program verification, reasoning about recursive data structures remains as a challenge for verification tools and their backends such as SMT and CHC solvers. To address the challenge, we introduce the notion of symbolic automatic relations (SARs), which combines symbolic automata and automatic relations, and inherits their good properties such as the closure under Boolean operations. We consider the satisfiability problem for SARs, and show that it is undecidable in general, but that we can construct a sound (but incomplete) and automated satisfiability checker by a reduction to CHC solving. We discuss applications to SMT and CHC solving on data structures, and show the effectiveness of our approach through experiments.
△ Less
Submitted 17 August, 2021;
originally announced August 2021.
