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

Explore a groundbreaking presentation on the first fully abstract normal form bisimulation for call-by-value PCF (PCFv). Delve into the innovative labelled transition system (LTS) that combines elements from applicative bisimulation, environmental bisimulation, and game semantics. Discover how this model constructs traces corresponding to interactions with possible functional contexts, achieving completeness without semantic quotiening. Learn about the sound and complete technique for checking PCFv program equivalence, implemented in a bounded bisimulation checking tool. Examine known equivalences from literature and new examples tested with this tool. Gain insights into this work, originally presented at LICS 2023, as shared by researchers Nikos Tzevelekos, Vasileios Koutavas, and Yu-Yang Lin during the GALOP'24 conference.