Fully Abstract Normal Form Bisimulation for Call-by-Value PCF
We present the first fully abstract normal form bisimulation for call-by-value PCF (PCFv). 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...
