Fully Abstract Normal Form Bisimulation for Call-by-Value PCF

TL;DR

This paper introduces the first fully abstract normal form bisimulation for call-by-value PCF, combining various semantic techniques to accurately determine program equivalence, and implements a tool for practical checking.

Contribution

It presents a novel fully abstract bisimulation model for call-by-value PCF that avoids semantic quotiening and integrates multiple semantic approaches.

Findings

The model is sound and complete for PCF_v program equivalence.

A bisimulation checking tool was implemented and tested successfully.

The approach handles both known and new program equivalences.

Abstract

We present the first fully abstract normal form bisimulation for call-by-value PCF (PCF$_{\textsf{v}}$). Our model is based on a labelled transition system (LTS) that combines elements from applicative bisimulation, environmental bisimulation and game semantics. In order to obtain completeness while avoiding the use of semantic quotiening, the LTS constructs traces corresponding to interactions with possible functional contexts. The model gives rise to a sound and complete technique for checking of PCF$_{\textsf{v}}$ program equivalence, which we implement in a bounded bisimulation checking tool. We test our tool on known equivalences from the literature and new examples.