Modeling Reachability Types with Logical Relations

TL;DR

This paper introduces a semantic model for reachability types using logical relations, enabling analysis of type soundness, termination, effect safety, and program equivalence in higher-order, mutable languages.

Contribution

It provides the first semantic framework for reachability types, extending their analysis to properties like termination, effect safety, and program equivalence.

Findings

Semantic type soundness established for reachability types.

Framework supports reasoning about termination with higher-order state.

Ensures effect safety and correctness of program reordering.

Abstract

Reachability types are a recent proposal to bring Rust-style reasoning about memory properties to higher-level languages, with a focus on higher-order functions, parametric types, and shared mutable state -- features that are only partially supported by current techniques as employed in Rust. While prior work has established key type soundness results for reachability types using the usual syntactic techniques of progress and preservation, stronger metatheoretic properties have so far been unexplored. This paper presents an alternative semantic model of reachability types using logical relations, providing a framework in which we study key properties of interest: (1) semantic type soundness, including of not syntactically well-typed code fragments, (2) termination, especially in the presence of higher-order state, (3) effect safety, especially the absence of observable mutation, and, finally, (4) program equivalence, especially reordering of non-interfering expressions for parallelization or compiler optimization.