Logical Bisimulations and Functional Languages

Developing a theory of bisimulation in higher-order languages can be hard. Particularly challenging can be the proof of congruence and, related to this, enhancements of the bisimulation proof method with “upto context” techniques. We present logical bisimulations, a form of bisimulation for higher-order languages, in which the bisimulation clause is somehow reminiscent of logical relations. We consider purely functional languages, in particular untyped call-by-name and call-by-value lambda-calculi, and, in each case: we present the basic properties of logical bisimilarity, including congruence; we show that it coincides with contextual equivalence; we develop some up-to techniques, including up-to context, as examples of possible enhancements of the associated bisimulation method.

• Type: Conference
• Year: 2007
• Where: FSEN
• Authors: Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
• Keywords: Bisimulation, Bisimulation Clause, Bisimulation Proof Method, FSEN 2007