An Interactive Proof of Termination for a Concurrent $\lambda$-calculus with References and Explicit Substitutions

TL;DR

This paper presents a typed, concurrent lambda-calculus with references and explicit substitutions, providing an interactive proof of termination that combines reducibility techniques with game semantics-inspired properties.

Contribution

It introduces a novel interactive proof method for termination in a concurrent lambda-calculus with references and explicit substitutions.

Findings

Achieves strong normalization for the calculus

Develops an interactive proof technique inspired by game semantics

Ensures safety properties in a concurrent setting

Abstract

In this paper we introduce a typed, concurrent $\lambda$-calculus with references featuring explicit substitutions for variables and references. Alongside usual safety properties, we recover strong normalization. The proof is based on a reducibility technique and an original interactive property reminiscent of the Game Semantics approach.