coFJ中的声音正则共现（CS PL）---蔡秋纯

本文的目的是为本机支持循环数据结构的创建和操作的编程范式提供坚实的基础。为此，我们描述了coFJ，它是一种类似Java的微积分，其中对象可以是无限的，方法配备了一个codefinition（另一种主体）。我们提出了一个抽象的微积分语义学，它是基于一个具有球的推理系统框架。在具有这种语义的coFJ中，有限对象上的FJ递归方法也可以扩展到无限对象，并通过指定一个codefinition来按照程序员的要求进行操作。我们还描述了一种可直接在编程语言中实现的操作语义，并证明了这种语义相对于抽象语义的合理性。

原文标题：Sound Regular Corecursion in coFJ

原文：The aim of the paper is to provide solid foundations for a programming paradigm natively supporting the creation and manipulation of cyclic data structures. To this end, we describe coFJ, a Java-like calculus where objects can be infinite and methods are equipped with a codefinition (an alternative body). We provide an abstract semantics of the calculus based on the framework of inference systems with corules. In coFJ with this semantics, FJ recursive methods on finite objects can be extended to infinite objects as well, and behave as desired by the programmer, by specifying a codefinition. We also describe an operational semantics which can be directly implemented in a programming language, and prove the soundness of such semantics with respect to the abstract one.

原文作者：Davide Ancona, Pietro Barbieri, Francesco Dagnino, Elena Zucca

原文地址：https://arxiv.org/abs/2005.14085