Fully abstract encodings of \(\lambda\)-calculus in HOcore through abstract machines. (English) Zbl 07906365
Summary: We present fully abstract encodings of the call-by-name and call-by-value \(\lambda\)-calculus into HOcore, a minimal higher-order process calculus with no name restriction. We consider several equivalences on the \(\lambda\)-calculus side – normal-form bisimilarity, applicative bisimilarity, and contextual equivalence – that we internalize into abstract machines in order to prove full abstraction of the encodings. We also demonstrate that this technique scales to the \(\lambda\mu\)-calculus, i.e., a standard extension of the \(\lambda\)-calculus with control operators.
Keywords:
lambda calculus; process calculi; abstract machine; control operator; bisimilarity; full abstractionReferences:
| [1] | Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A functional correspondence between evaluators and abstract machines. In Dale Miller, editor, Proceedings of the Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP’03), pages 8-19, Uppsala, Sweden, August 2003. ACM Press. |
| [2] | Beniamino Accattoli. Evaluating functions as processes. In Rachid Echahed and Detlef Plump, editors, Proceedings 7th International Workshop on Computing with Terms and Graphs, TERM-GRAPH 2013, volume 110 of EPTCS, pages 41-55, Rome, Italy, March 2013. · Zbl 1464.68219 |
| [3] | Zena M. Ariola and Hugo Herbelin. Control reduction theories: the benefit of structural substitu-tion. Journal of Functional Programming, 18(3):373-419, 2008. · Zbl 1138.68020 |
| [4] | Roberto M. Amadio. A decompilation of the pi-calculus and its application to termination. CoRR, abs/1102.2339, 2011. |
| [5] | Samson Abramsky and C.-H. Luke Ong. Full abstraction in the lazy lambda calculus. Information and Computation, 105:159-267, 1993. · Zbl 0779.03003 |
| [6] | Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundation of Mathematics. North-Holland, revised edition, 1984. [BBL + 17] Ma lgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, and Alan Schmitt. Fully abstract encodings of λ-calculus in hocore through abstract machines. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. doi:10.1109/LICS.2017.8005118. · Zbl 1452.03041 · doi:10.1109/LICS.2017.8005118 |
| [7] | Emmanuel Beffara. Functions as proofs as processes. CoRR, abs/1107.4160, 2011. |
| [8] | Martin Berger, Kohei Honda, and Nobuko Yoshida. Sequentiality and the pi-calculus. In Samson Abramsky, editor, Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, number 2044 in Lecture Notes in Computer Science, pages 29-45, Kraków, Poland, May 2001. Springer-Verlag. · Zbl 0981.68037 |
| [9] | Dariusz Biernacki and Sergueï Lenglet. Applicative bisimilarities for call-by-name and call-by-value λµ-calculus. In Bart Jacobs, Alexandra Silva, and Sam Staton, editors, Proceedings of the 30th Annual Conference on Mathematical Foundations of Programming Semantics(MFPS XXX), volume 308 of ENTCS, pages 49-64, Ithaca, NY, USA, June 2014. · Zbl 1337.68056 |
| [10] | Matteo Cimini, Claudio Sacerdoti Coen, and Davide Sangiorgi. Functions as processes: Termina-tion and the λµμ-calculus. In Martin Wirsing, Martin Hofmann, and Axel Rauschmayer, editors, Trustworthly Global Computing -5th International Symposium, TGC 2010,. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
