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.

翻译：我们提出了首个针对 call-by-value PCF（PCF$_{\textsf{v}}$）的全抽象范式互模拟。该模型基于一个结合了应用互模拟、环境互模拟与博弈语义元素的标记转换系统（LTS）。为在避免使用语义商化的情况下获得完备性，LTS 构造了与可能的函数上下文交互相对应的迹。该模型提供了一种用于检查 PCF$_{\textsf{v}}$ 程序等价性的可靠且完备的技术，我们将其实现为一个有界互模拟检查工具。我们在文献中已知的等价性实例及新例子上对该工具进行了测试。