ATheor yo fOperationa lEquivalenc efor Interaction Nets
Maribel Fernández, Ian Mackie · 2000
The notion of contextual equivalence is fundamental in the theory of programming languages. By setting up a notion of bisimilarity, and showing that it coincides with contextual equivalence, one obtains a simple coinductive proof techniqu efo rshowin gtha ttw oprogram sar eequivalen ti nal lcontexts .I nthis paper we apply these (now standard) techniques to interactions nets, a graphical programming language characterized by local reduction. This work generalizes previous studies of operational equivalence in interaction nets since it can be applied to untyped systems, thus all systems of interaction nets are captured.