Simple Reference Immutability for System F-sub

TL;DR

This paper extends System F-sub with reference immutability, analyzing its interaction with higher-order functions and subtyping, and proves its soundness and safety in a formal calculus.

Contribution

It introduces System F-sub-M, a formal calculus integrating reference immutability with polymorphism and subtyping, and proves its core properties.

Findings

System F-sub-M encodes reference immutability as an extension of F-sub.

The calculus satisfies soundness and immutability safety properties.

The work bridges object-oriented and functional language features.

Abstract

Reference immutability is a type based technique for taming mutation that has long been studied in the context of object-oriented languages, like Java. Recently, though, languages like Scala have blurred the lines between functional programming languages and object oriented programming languages. We explore how reference immutability interacts with features commonly found in these hybrid languages, in particular with higher-order functions -- polymorphism -- and subtyping. We construct a calculus System F-sub-M which encodes a reference immutability system as a simple extension of F-sub and prove that it satisfies the standard soundness and immutability safety properties.