Trace semantics for polymorphic references

TL;DR

This paper develops a trace semantics model for a polymorphic language with references, addressing parametricity violations and achieving full abstraction under certain conditions.

Contribution

It introduces a novel operational game semantics for polymorphic references, incorporating nominal interpretation to handle parametricity violations.

Findings

Model is sound for the full language

Achieves full abstraction for a large fragment

Addresses parametricity violations with semantic recoding

Abstract

We introduce a trace semantics for a call-by-value language with full polymorphism and higher-order references. This is an operational game semantics model based on a nominal interpretation of parametricity whereby polymorphic values are abstracted with special kinds of names. The use of polymorphic references leads to violations of parametricity which we counter by closely recoding the disclosure of typing information in the semantics. We prove the model sound for the full language and strengthen our result to full abstraction for a large fragment where polymorphic references obey specific inhabitation conditions.