Oct. 5, 2017, noon

Normal-form bisimilarity is a simple, easy-to-use behavioral equivalence that relates terms in lambda-calculi by decomposing their normal forms into bisimilar subterms. Besides, they allow for powerful up-to techniques, such as bisimulation up to context, which simplify bisimulation proofs even further. However, proving soundness of these relations becomes complicated in the presence of eta-expansion and usually relies on ad hoc proof methods which depend on the language. In this talk, I will present a more systematic proof method to show that an extensional normal-form bisimilarity along with its corresponding bisimulation up to context are sound.

The talk is based on our recent paper (of the same title) with Dariusz Biernacki and Sergueï Lenglet.