Abstract
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 technique for showing that two programs are equivalent in all contexts. In this 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abramsky, S.: The lazy λ-calculus. In: Turner, D.A. (ed.) Research Topics in Functional Programming, ch. 4, pp. 65–117. AddisonWesley, London (1990)
Fernández, M., Mackie, I.: Coinductive techniques for operational equivalence of interaction nets. In: Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS 1998), pp. 321–332. IEEE Computer Society Press, Los Alamitos (1998)
Fernández, M., Mackie, I.: A calculus for interaction nets. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702. Springer, Heidelberg (1999)
Gonthier, G., Abadi, M., Lévy, J.-J.: The geometry of optimal lambda reduction. In: Proceedings of the 19th ACM Symposium on Principles of Programming Languages (POPL 1992), pp. 15–26. ACM Press, New York (1992)
Howe, D.J.: Proving congruence of bisimulation in functional programming languages. Information and Computation 124(2), 103–112 (1996)
Khalil, L.: Mémoire de DEA SPP (1999), Available at http://www.dmi.ens.fr/~khalil
Lafont, Y.: Interaction nets. In: Proceedings of the 17th ACM Symposium on Principles of Programming Languages (POPL 1990), pp. 95–108. ACM Press, New York (1990)
Lafont, Y.: Interaction combinators. Information and Computation 137(1), 69–101 (1997)
Mackie, I.: YALE: Yet another lambda evaluator based on interaction nets. In: Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming (ICFP 1998), pp. 117–128. ACM Press, New York (1998)
Pitts, A.M.: Operationally-based theories of program equivalence. In: Dybjer, P., Pitts, A.M. (eds.) Semantics and Logics of Computation (Publications of the Newton Institute), pp. 241–298. Cambridge University Press, Cambridge (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fernández, M., Mackie, I. (2000). A Theory of Operational Equivalence for Interaction Nets. In: Gonnet, G.H., Viola, A. (eds) LATIN 2000: Theoretical Informatics. LATIN 2000. Lecture Notes in Computer Science, vol 1776. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10719839_44
Download citation
DOI: https://doi.org/10.1007/10719839_44
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67306-4
Online ISBN: 978-3-540-46415-0
eBook Packages: Springer Book Archive