POPL 2024 (series) / GALOP 2024 (series) / GALOP 2024 /
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 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 PCFv program equivalence, which we implement in a bounded bisimulation checking tool. We test our tool on known equivalences from the literature and new examples. This work was presented in LICS 2023.
Sun 14 JanDisplayed time zone: London change
Sun 14 Jan
Displayed time zone: London change
09:00 - 10:30 | |||
09:00 45mKeynote | On Interaction, Efficiency, and Reversibility GALOP Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis | ||
09:45 22mTalk | Normal Form Bisimulations by Value GALOP Beniamino Accattoli Inria & Ecole Polytechnique, Adrienne Lancelot Inria, LIX Ecole Polytechnique, IRIF Université Paris Cité, Claudia Faggian Université de Paris & CNRS | ||
10:08 22mTalk | Fully Abstract Normal Form Bisimulation for Call-by-Value PCF GALOP Nikos Tzevelekos Queen Mary University of London, Vasileios Koutavas Trinity College Dublin, Yu-Yang Lin Queen Mary University of London |