Document Open Access Logo

Strong Bisimulation for Control Operators (Invited Talk)

Authors Delia Kesner, Eduardo Bonelli, Andrés Viso

PDF
Thumbnail PDF

File

LIPIcs.CSL.2020.4.pdf
  • Filesize: 0.67 MB
  • 23 pages

Document Identifiers

Author Details

Delia Kesner
  • IRIF, Université de Paris and CNRS, France
  • Institut Universitaire de France (IUF), France
Eduardo Bonelli
  • Stevens Institute of Technology, Hoboken, NJ, USA
Andrés Viso
  • Universidad de Buenos Aires, Argentina
  • Universidad Nacional de Quilmes, Bernal, Buenos Aires, Argentina

Funding

This work was partially supported by LIA INFINIS, and the ECOS-Sud program PA17C01.

Acknowledgements

To Olivier Laurent for fruitful discussions.

Cite AsGet BibTex

Delia Kesner, Eduardo Bonelli, and Andrés Viso. Strong Bisimulation for Control Operators (Invited Talk). In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CSL.2020.4

Abstract

The purpose of this paper is to identify programs with control operators whose reduction semantics are in exact correspondence. This is achieved by introducing a relation ≃, defined over a revised presentation of Parigot’s λμ-calculus we dub ΛM. Our result builds on two fundamental ingredients: (1) factorization of λμ-reduction into multiplicative and exponential steps by means of explicit term operators of ΛM, and (2) translation of ΛM-terms into Laurent’s polarized proof-nets (PPN) such that cut-elimination in PPN simulates our calculus. Our proposed relation ≃ is shown to characterize structural equivalence in PPN. Most notably, ≃ is shown to be a strong bisimulation with respect to reduction in ΛM, i.e. two ≃-equivalent terms have the exact same reduction semantics, a result which fails for Regnier’s σ-equivalence in λ-calculus as well as for Laurent’s σ-equivalence in λμ.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Linear logic
  • Theory of computation → Operational semantics
Keywords
  • Lambda-mu calculus
  • proof-nets
  • strong bisimulation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Beniamino Accattoli. Compressing Polarized Boxes. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 428-437. IEEE Computer Society, 2013. URL: http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6570844.
  2. Beniamino Accattoli. Proof-Nets and the Linear Substitution Calculus. In Bernd Fischer and Tarmo Uustalu, editors, Theoretical Aspects of Computing - ICTAC 2018 - 15th International Colloquium, Stellenbosch, South Africa, October 16-19, 2018, Proceedings, volume 11187 of Lecture Notes in Computer Science, pages 37-61. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02508-3_3.
  3. Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. Distilling abstract machines. In Johan Jeuring and Manuel M. T. Chakravarty, editors, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014, pages 363-376. ACM, 2014. URL: https://doi.org/10.1145/2628136.2628154.
  4. Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi. A nonstandard standardization theorem. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 659-670. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535886.
  5. Beniamino Accattoli and Delia Kesner. The Permutative λ-Calculus. In Nikolaj Bjørner and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings, volume 7180 of Lecture Notes in Computer Science, pages 23-36. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28717-6_5.
  6. Philippe Audebaud. Explicit Substitutions for the Lambda-Mu-Calculus. Technical report, LIP, ENS Lyon, 1994. Google Scholar
  7. Eduardo Bonelli, Delia Kesner, and Andrés Viso. Strong Bisimulation for Control Operators. CoRR, abs/1906.09370, 2019. URL: http://arxiv.org/abs/1906.09370.
  8. Roberto Di Cosmo, Delia Kesner, and Emmanuel Polonowski. Proof-Nets and Explicit Substitutions. In Jerzy Tiuryn, editor, Foundations of Software Science and Computation Structures, Third International Conference, FOSSACS 2000, Held as Part of the Joint European Conferences on Theory and Practice of Software,ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings, volume 1784 of Lecture Notes in Computer Science, pages 63-81. Springer, 2000. URL: https://doi.org/10.1007/3-540-46432-8_5.
  9. Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Martin Odersky and Philip Wadler, editors, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, September 18-21, 2000., pages 233-243. ACM, 2000. URL: https://doi.org/10.1145/351240.351262.
  10. Vincent Danos and Laurent Regnier. Proof-nets and the Hilbert space. In Workshop on Advances in Linear Logic, New York, NY, USA, page 307–328. Cambridge University Press, 1995. Google Scholar
  11. Philippe de Groote. On the Relation between the Lambda-Mu-Calculus and the Syntactic Theory of Sequential Control. In Frank Pfenning, editor, Logic Programming and Automated Reasoning, 5th International Conference, LPAR'94, Kiev, Ukraine, July 16-22, 1994, Proceedings, volume 822 of Lecture Notes in Computer Science, pages 31-43. Springer, 1994. URL: https://doi.org/10.1007/3-540-58216-9_27.
  12. Jean-Yves Girard. Linear Logic. Theoretical Computer Science, 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  13. Timothy Griffin. A Formulae-as-Types Notion of Control. In Frances E. Allen, editor, Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990, pages 47-58. ACM Press, 1990. URL: https://doi.org/10.1145/96709.96714.
  14. Tom Gundersen, Willem Heijltjes, and Michel Parigot. Atomic Lambda Calculus: A Typed Lambda-Calculus with Explicit Sharing. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 311-320. IEEE Computer Society, 2013. Google Scholar
  15. Thérèse Hardin. Confluence results for the strong pure categorical logic CCL; λ-calculi as subsystems of CCL. tcs, 65, 1989. Google Scholar
  16. Kohei Honda and Olivier Laurent. An exact correspondence between a typed pi-calculus and polarised proof-nets. Theoretical Computer Science, 411(22-24):2223-2238, 2010. Google Scholar
  17. Delia Kesner. A Theory of Explicit Substitutions with Safe and Full Composition. Logical Methods in Computer Science, 5(3), 2009. URL: http://arxiv.org/abs/0905.2539.
  18. Delia Kesner and Stéphane Lengrand. Extending the Explicit Substitution Paradigm. In Jürgen Giesl, editor, Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, volume 3467 of Lecture Notes in Computer Science, pages 407-422. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-32033-3_30.
  19. Delia Kesner and Pierre Vial. Types as Resources for Classical Natural Deduction. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK, volume 84 of LIPIcs, pages 24:1-24:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.24.
  20. Delia Kesner and Pierre Vial. Non-idempotent types for classical calculi in natural deduction style. Logical Methods in Computer Science, 2019. To appear. Google Scholar
  21. Olivier Laurent. Krivine’s abstract machine and the lambda-mu calculus. URL: https://perso.ens-lyon.fr/olivier.laurent/lmkamen.pdf.
  22. Olivier Laurent. A study of polarization in logic. Theses, Université de la Méditerranée - Aix-Marseille II, March 2002. URL: https://tel.archives-ouvertes.fr/tel-00007884.
  23. Olivier Laurent. Polarized proof-nets and lambda-μ-calculus. Theoretical Computer Science, 290(1):161-188, 2003. Google Scholar
  24. Olivier Laurent and Laurent Regnier. About Translations of Classical Logic into Polarized Linear Logic. In 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings, pages 11-20. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/LICS.2003.1210040.
  25. Michel Parigot. Classical Proofs as Programs. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, KGC'93, Brno, Czech Republic, August 24-27, 1993, Proceedings, volume 713 of Lecture Notes in Computer Science, pages 263-276. Springer, 1993. URL: https://doi.org/10.1007/BFb0022575.
  26. Emmanuel Polonovski. Subsitutions explicites, logique et normalisation. (Explicit substitutions, logic and normalization). PhD thesis, Paris Diderot University, France, 2004. URL: https://tel.archives-ouvertes.fr/tel-00007962.
  27. Laurent Regnier. Une équivalence sur les lambda-termes. Theoretical Computer Science, 2(126):281-292, 1994. Google Scholar
  28. Steffen van Bakel and Maria Grazia Vigliotti. A fully-abstract semantics of lambda-mu in the pi-calculus. In Paulo Oliva, editor, Proceedings Fifth International Workshop on Classical Logic and Computation, CL&C 2014, Vienna, Austria, July 13, 2014., volume 164 of EPTCS, pages 33-47, 2014. URL: https://doi.org/10.4204/EPTCS.164.3.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact