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

on YouTube ↗23m

" summary

Presents the first fully abstract normal form bisimulation for call-by-value PCF, built from an LTS that mixes applicative, environmental and game-semantic moves and explicitly constructs traces representing interactions with functional contexts. Proves soundness and completeness: contextual equivalence iff bisimilarity in the LTS. Ships a bounded bisimulation checking tool that runs the on-the-fly LTS, finds distinguishing traces for inequivalence and verifies equivalences on known literature examples and new cases; work appears from LICS 2023 and supports extracting contexts from traces.

AI-written summary · about

" chapters (12)

1. 0:00Introduction
2. 1:07Program equivalence in call-by-value PCF
3. 3:56Pure vs impure equivalences
4. 7:09Full abstraction in PCF history
5. 8:55Games semantics and contextual equivalence
6. 10:41Normal form bisimulation background
7. 12:25Language features and external functions
8. 13:30Labeled transition system for open terms
9. 16:43Trace memory and opponent restrictions
10. 18:10Bisimulation definition and proof
11. 19:33Summary and tool demo
12. 20:41Q&A