论文标题

在COFJ中听起来常规的cocursion

Sound Regular Corecursion in coFJ

论文作者

Ancona, Davide, Barbieri, Pietro, Dagnino, Francesco, Zucca, Elena

论文摘要

本文的目的是为编程范式提供坚实的基础,从而在本质上支持循环数据结构的创建和操纵。为此,我们描述了COFJ,这是一种类似Java的演算,其中可以无限的对象,并配备了代码文件(替代体)。我们根据带有芯的推理系统的框架提供了微积分的抽象语义。在具有此语义的COFJ中,有限对象上的FJ递归方法也可以扩展到无限对象,并通过指定代码文件来按照程序员的要求来表现。我们还描述了一种可以直接以编程语言实现的操作语义,并证明了这种语义相对于抽象语言的健全性。

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.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源