This model demonstrates sound program equivalence in call-by-value PCF, suggesting new approaches in verification.
We present the first fully abstract normal form bisimulation for call-by-value PCF (PCF \(ᵥ \) ). 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 quotienting, 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 \(ᵥ \) program equivalence, which we implement in a bounded bisimulation checking tool. We test our tool on known equivalences from the literature and new examples.
No takes yet. Share an insight, caveat, or question.
Koutavas et al. (2025) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: