(Definitely not) Boring interaction abstract machines

The interaction abstract machine is an automata-theoretic implementation of Girard’s geometry of interaction. We study one of its two formulations for the λ -calculus, namely the one obtained from the so-called call-by-value (or “boring”) translation of intuitionistic logic into linear logic. We prove the correctness of the resulting call-by-name machine, at the same time establishing an improvement bisimulation with Krivine’s abstract machine. The proof makes essential use of the definition of a novel relational property linking configurations of the two machines. Finally, exploiting the correspondence with non-idempotent intersection types, we prove that the interaction abstract machines coming from Girard’s two translations are strongly bisimilar.