Research in programming languages mostly proceeds language by language. This in particular means that key ideas are often introduced for one typical language, and must then be adapted to other languages.

A prominent example of this is Howe's method for proving that applicative bisimilarity, a notion of program equivalence in call-by-name λ-calculus, is a congruence. This method has been adapted to call-by-value λ-calculus, PCF, λ-calculus with delimited continuations, higher-order π-calculus,…

In this work, using category theory, we establish an abstract congruence theorem for applicative bisimilarity, of which most existing adaptations of Howe's method are instances. The framework is both simpler and more general than our previous attempts.

This is joint work with Ambroise Lafont.