Complete trace models of state and control

TL;DR

This paper develops fully abstract trace models for a hierarchy of typed call-by-value languages with various features like higher-order references and callcc, using operational game semantics to analyze their interactions.

Contribution

It constructs the first fully abstract trace model for the most expressive language with higher-order references and callcc, and refines models for simpler cases by analyzing the impact of feature suppression.

Findings

Fully abstract trace model for languages with both higher-order references and callcc

Operational explanation of visibility and bracketing conditions

Refined models for languages with suppressed features

Abstract

We consider a hierarchy of four typed call-by-value languages with either higher-order or ground-type references and with either callcc or no control operator.Our first result is a fully abstract trace model for the most expressive setting, featuring both higher-order references and callcc, constructed in the spirit of operational game semantics. Next we examine the impact of suppressing higher-order references and callcc in contexts and provide an operational explanation for the game-semantic conditions known as visibility and bracketing respectively.This allows us to refine the original model to provide fully abstract trace models of interaction with contexts that need not use higher-order references or callcc. Along the way, we discuss the relationship between error- and termination-based contextual testing in each case, and relate the two to trace and complete trace equivalence respectively.Overall, the paper provides a systematic development of operational game semantics for all four cases, which represent the state-based face of the so-called semantic cube.