An affine-intuitionistic system of types and effects: confluence and termination

An affine-intuitionistic system of types and effects: confluence and termination

We present an affine-intuitionistic system of types and effects which can be regarded as an extension of Barber-Plotkin Dual Intuitionistic Linear Logic to multi-threaded programs with effects. In the system, dynamically generated values such as references or channels are abstracted into a finite set of regions. We introduce a discipline of region usage that entails the confluence (and hence determinacy) of the typable programs. Further, we show that a discipline of region stratification guarantees termination.

Certifying Confluence Proofs via Relative Termination and Rule Labeling

The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based on the interplay of relative termination and the rule labeling in the theorem prover Isabelle. Moreover, we report on the integration of this result into the certifier CeTA, facilitating the checking of confluence certificates based on decreasing diagrams. The power of the method is illustrated by an experimental evaluation on a (standard) collection of confluence problems.

高阶重写系统的终止与合流

Termination and Confluence of Higher-Order Rewrite Systems

在过去的20年里，已经提出了几种高阶重写方法，其中包括Klop的组合重写系统（CRS），Nipkow的高阶重写系统（HRS）以及Jouannaud和Okada的高阶代数规约语言，其中只有最后一种考虑了类型化项。Jouannaud、Okada和本文作者将后一种方法推广到归纳数据类型系统（IDTS）。在本文中，我们扩展了IDTS与CRS高阶模式匹配机制，导致简单类型的CRS。然后，我们展示了如何终止标准开发的IDTS与一阶模式匹配，称为一般模式，可以扩展，以证明强规范化的IDTS与高阶模式匹配。接下来，我们将统一的方法与HRS进行比较。我们首先证明了扩展的一般模式也可以适用于人力资源系统。其次，我们展示了如何Nipkow的高阶临界对分析技术证明当地的融合可以应用于IDTS。

直觉主义强Löb逻辑的新演算：强终止性与消割，形式化

A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised

本文为直觉主义强Löb逻辑提出新相继式演算，实现强终止的向后搜索与句法消割，并在Coq中形式化验证。

Clausal Resolution for Modal Logics of Confluence

We present a clausal resolution-based method for normal multimodal logics of confluence, whose Kripke semantics are based on frames characterised by appropriate instances of the Church-Rosser property. Here we restrict attention to eight families of such logics. We show how the inference rules related to the normal logics of confluence can be systematically obtained from the parametrised axioms that characterise such systems. We discuss soundness, completeness, and termination of the method. In particular, completeness can be modularly proved by showing that the conclusions of each newly added…

The Certification Problem Format

We provide an overview of CPF, the certification problem format, and explain some design decisions. Whereas CPF was originally invented to combine three different formats for termination proofs into a single one, in the meanwhile proofs for several other properties of term rewrite systems are also expressible: like confluence, complexity, and completion. As a consequence, the format is already supported by several tools and certifiers. Its acceptance is also demonstrated in international competitions: the certified tracks of both the termination and the confluence competition utilized CPF as e…