Formalizing $\varphi$-calculus: a purely object-oriented calculus of decorated objects

TL;DR

This paper formalizes an untyped, purely object-oriented calculus of decorated objects, demonstrating its confluence, providing an abstract machine for evaluation, and establishing a translation to lambda calculus with records.

Contribution

It introduces a novel untyped calculus based on decoration, independent of lambda calculus, with proven confluence and a call-by-name evaluation machine.

Findings

Proves the calculus is confluent (Church-Rosser property)

Develops an abstract machine for call-by-name evaluation

Provides a sound translation to lambda calculus with records

Abstract

Many calculi exist for modelling various features of object-oriented languages. Many of them are based on $\lambda$-calculus and focus either on statically typed class-based languages or dynamic prototype-based languages. We formalize untyped calculus of decorated objects, informally presented by Bugayenko, which is defined in terms of objects and relies on decoration as a primary mechanism of object extension. It is not based on $\lambda$-calculus, yet with only four basic syntactic constructions is just as complete. We prove the calculus is confluent (i.e. possesses Church-Rosser property), and introduce an abstract machine for call-by-name evaluation. Finally, we provide a sound translation to $\lambda$-calculus with records.