pi演算的反编译及其在终止性中的应用

Termination Analysis for the $π$-Calculus by Reduction to Sequential Program Termination

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 …

An Interactive Proof of Termination for a Concurrent $λ$-calculus with References and Explicit Substitutions

In this paper we introduce a typed, concurrent $λ$-calculus with references featuring explicit substitutions for variables and references. Alongside usual safety properties, we recover strong normalization. The proof is based on a reducibility technique and an original interactive property reminiscent of the Game Semantics approach.

A Calculus for Modular Loop Acceleration and Non-Termination Proofs

Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs. To this end, a variety of acceleration techniques has been proposed. However, so far all of them have been monolithic, i.e., a single loop could not be accelerated using a combination of several different acceleration techniques. In contrast, we present a calculus that allows for combining acceleration techniques in a modular way and we show how to integrate many existing acceleration techniques into our calculus. Moreover, we propose two novel acceleration techniques that can be inc…

无类型λ演算中的按值调用终止

Call-by-value Termination in the Untyped lambda-calculus

一个全自动的算法开发能够显示，一个给定的无类型的可扩展表达式的评估将终止CBV（按值调用）。本文分两步将一阶程序中的“变长原理”推广到任意无类型的可达表达式。第一步足以显示单个独立lambda;-表达式的CBV终止。第二个足以显示CBV终止的任何成员的一个正规的一组的Adjuda表达式，定义了一个树语法。（一个简单的例子是最小函数，当应用于任意的丘奇数时。该算法是合理的，并在本文中证明。停机问题的不可判定性意味着任何合理的算法都必然是不完整的：某些可达表达式实际上可能在CBV求值下终止，但不被认为是终止的。终止算法的强度相当高。它证明了许多有趣和有用的通用递归算法，包括相互递归和参数交换的程序，以及Colson的“最小值”算法。此外，我们的无类型方法允许使用Y组合子，因此可以识别为终止PCF的大量子集。

An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear $π$-Calculus

Fair termination is the property of programs that may diverge "in principle" but that terminate "in practice", i.e. under suitable fairness assumptions concerning the resolution of non-deterministic choices. We study a conservative extension of $μ$MALL$^\infty$, the infinitary proof system of the multiplicative additive fragment of linear logic with least and greatest fixed points, such that cut elimination corresponds to fair termination. Proof terms are processes of $π$LIN, a variant of the linear $π$-calculus with (co)recursive types into which binary and (some) multiparty sessions can be e…

控制算子的完全按值调用演算 II：强终止性

Complete Call-by-Value Calculi of Control Operators II: Strong Termination

本文刻画了完全按值调用 lambda-mu 演算的强终止性，基于 CPS 语义和并-交集类型系统，证明了强可规范化性的充要条件。