文章基本信息

标题：Sound Regular Corecursion in coFJ
本地全文：下载
作者：Davide Ancona ; Pietro Barbieri ; Francesco Dagnino 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：166
页码：1-28
DOI：10.4230/LIPIcs.ECOOP.2020.1
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Operational semantics; coinduction; programming paradigms; regular terms