Normal Form Bisimulations by Value

on YouTube ↗22m

" summary

Defines a new call-by-value normal-form bisimilarity, net bisimilarity, built on the value substituent calculus of aatan Pini; proves net is included (strictly) in contextual equivalence by adapting Lassen’s compatibility method and shows net identifies all call-by-value meaningless terms. Compares net to Lassen’s enf (Lassen) bisimilarity: they are incomparable, there is no simple union, and net fails to validate Moggi’s monadic laws (so it omits some identity/ETA value equalities). Also relates both to Ehrhard’s relational/type semantics and to proof-net commutation phenomena.

AI-written summary · about

" chapters (14)

1. 0:00Normal Form Bisimulations by Value
2. 1:27Call by Value vs Call by Name
3. 3:51Open terms in Plotkin's Call by Value
4. 5:18Contextual equivalence limits
5. 7:25Normal form bisimilarity technique
6. 8:49Normal form bisimilarity in Call by Name
7. 10:12Existing Call by Value bisimilarity
8. 11:57Naive Call by Value bisimulation
9. 12:40Net bisimulation in Open Call by Value
10. 14:28Compatibility via Lassen's method
11. 15:32Type equivalence via intersection types
12. 17:44Operational game semantics role
13. 19:54Summary and open questions
14. 21:02Q&A: Untyped Call by Value game semantics