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

Sangiorgi’s normal form bisimilarity is call-by-name, identifies all the call-by-name meaningless terms, and rests on open terms in its definition. The literature contains a normal form bisimilarity for the call-by-value λ-calculus, Lassen’s enf bisimilarity, which validates all of Moggi’s monadic laws. The starting point of this work is the observation that enf bisimilarity is not the call-by-value equivalent of Sangiorgi’s, because it does not identify the call-by-value meaningless terms. The issue has to do with open terms. We then develop a new call-by-value normal form bisimilarity, deemed net bisimilarity, by exploiting an existing formalism for dealing with open terms in call-by-value. It turns out that enf and net bisimilarities are incomparable, as net bisimilarity identifies meaningless terms but it does not validate Moggi’s laws. Moreover, there is no easy way to merge them. To better understand the situation, we provide a detailed analysis of the rich range of possible call-by-value normal form bisimilarities, relating them to Ehrhard’s call-by-value relational semantics.

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