Towards univalent reference types

TL;DR

This paper introduces a denotational semantics for reference types within univalent foundations, revealing how univalence influences program invariance and equivalences in mutable state modeling.

Contribution

It develops a novel semantic framework for reference types in univalent type theory, highlighting univalence's role in ensuring computation invariance under heap symmetries.

Findings

Univalence impacts the semantics of mutable state.

All computations become invariant under heap symmetries.

New program equivalences emerge in univalent models.

Abstract

We develop a denotational semantics for general reference types in an impredicative version of guarded homotopy type theory, an adaptation of synthetic guarded domain theory to Voevodsky's univalent foundations. We observe for the first time the profound impact of univalence on the denotational semantics of mutable state. Univalence automatically ensures that all computations are invariant under symmetries of the heap -- a bountiful source of program equivalences. In particular, even the most simplistic univalent model enjoys many new equations that do not hold when the same constructions are carried out in the universes of traditional set-level (extensional) type theory.