Isomorphisms of types in the presence of higher-order references

TL;DR

This paper characterizes type isomorphisms in a language with higher-order references using game semantics, proving a conjecture for finitely branching cases and revealing new isomorphisms in infinite cases.

Contribution

It solves Laurent's open problem by characterizing isomorphisms of finitely branching arenas and extends the understanding to infinite branching with natural numbers.

Findings

Finitely branching arenas are isomorphic iff they are geometrically the same (Laurent's forest isomorphism).

Provides an equational theory for type isomorphisms in a finitary language with higher-order references.

Laurent's conjecture fails for infinitely branching arenas, revealing new non-trivial isomorphisms.

Abstract

We investigate the problem of type isomorphisms in a programming language with higher-order references. We first recall the game-theoretic model of higher-order references by Abramsky, Honda and McCusker. Solving an open problem by Laurent, we show that two finitely branching arenas are isomorphic if and only if they are geometrically the same, up to renaming of moves (Laurent's forest isomorphism). We deduce from this an equational theory characterizing isomorphisms of types in a finitary language with higher order references. We show however that Laurent's conjecture does not hold on infinitely branching arenas, yielding a non-trivial type isomorphism in the extension of this language with natural numbers.