Sound Regular Corecursion in coFJ

TL;DR

This paper introduces coFJ, a calculus extending Java-like objects with support for infinite and cyclic data structures, providing a solid semantic foundation and operational semantics for such programming paradigms.

Contribution

It presents coFJ, a novel calculus with an abstract and operational semantics for cyclic data structures, enabling safe manipulation of infinite objects in a Java-like setting.

Findings

Abstract semantics based on inference systems with corules

Operational semantics that can be implemented in programming languages

Proof of soundness of the operational semantics

Abstract

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.