POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Sun 14 Jan 2024 10:08 - 10:30 at Lovelace Room - Session 1 Chair(s): Pierre Clairambault

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 Jan

Displayed time zone: London change

09:00 - 10:30
Session 1GALOP at Lovelace Room
Chair(s): Pierre Clairambault CNRS & LIS, Aix-Marseille Université
09:00
45m
Keynote
On Interaction, Efficiency, and Reversibility
GALOP
Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis
09:45
22m
Talk
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
22m
Talk
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