  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.
