Nothing Special   »   [go: up one dir, main page]
Document Open Access Logo

Formalizing Functions as Processes

Authors Beniamino Accattoli , Horace Blanc, Claudio Sacerdoti Coen

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.5.pdf
  • Filesize: 0.79 MB
  • 21 pages

Document Identifiers

Author Details

Beniamino Accattoli
  • Inria & LIX, École Poytechnique, Palaiseau, France
Horace Blanc
  • Independent researcher, Paris, France
Claudio Sacerdoti Coen
  • Alma Mater Studiorum - University of Bologna, Italy

Funding

Sacerdoti Coen has been supported by the INdAM-GNCS project "Proprietà qualitative e quantitative dei Sistemi Reversibili" and by the Cost Action CA20111 EuroProofNet.

Cite AsGet BibTex

Beniamino Accattoli, Horace Blanc, and Claudio Sacerdoti Coen. Formalizing Functions as Processes. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.5

Abstract

We present the first formalization of Milner’s classic translation of the λ-calculus into the π-calculus. It is a challenging result with respect to variables, names, and binders, as it requires one to relate variables and binders of the λ-calculus with names and binders in the π-calculus. We formalize it in Abella, merging the set of variables and the set of names, thus circumventing the challenge and obtaining a neat formalization. About the translation, we follow Accattoli’s factoring of Milner’s result via the linear substitution calculus, which is a λ-calculus with explicit substitutions and contextual rewriting rules, mediating between the λ-calculus and the π-calculus. Another aim of the formalization is to investigate to which extent the use of contexts in Accattoli’s refinement can be formalized.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Process calculi
  • Theory of computation → Operational semantics
  • Theory of computation → Automated reasoning
Keywords
  • Lambda calculus
  • pi calculus
  • proof assistants
  • binders
  • Abella

Metrics

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

Supplementary Materials

References

  1. Beniamino Accattoli. Proof pearl: Abella formalization of λ-calculus cube property. In Chris Hawblitzel and Dale Miller, editors, Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings, volume 7679 of Lecture Notes in Computer Science, pages 173-187. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-35308-6_15.
  2. Beniamino Accattoli. Evaluating functions as processes. In Rachid Echahed and Detlef Plump, editors, Proceedings 7th International Workshop on Computing with Terms and Graphs, TERMGRAPH 2013, Rome, Italy, 23th March 2013, volume 110 of EPTCS, pages 41-55, 2013. URL: https://doi.org/10.4204/EPTCS.110.6.
  3. 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.
  4. 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.
  5. Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi. A nonstandard standardization theorem. In 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.
  6. Beniamino Accattoli and Ugo Dal Lago. On the invariance of the unitary cost model for head reduction. In Ashish Tiwari, editor, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan, volume 15 of LIPIcs, pages 22-37. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.RTA.2012.22.
  7. Beniamino Accattoli and Ugo Dal Lago. (leftmost-outermost) beta reduction is invariant, indeed. Log. Methods Comput. Sci., 12(1), 2016. URL: https://doi.org/10.2168/LMCS-12(1:4)2016.
  8. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The machinery of interaction. In PPDP '20: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9-10 September, 2020, pages 4:1-4:15. ACM, 2020. URL: https://doi.org/10.1145/3414080.3414108.
  9. Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds, fully developed. J. Funct. Program., 30:e14, 2020. URL: https://doi.org/10.1017/S095679682000012X.
  10. Guillaume Ambal, Sergueï Lenglet, and Alan Schmitt. Hoπ in coq. J. Autom. Reason., 65(1):75-124, 2021. URL: https://doi.org/10.1007/s10817-020-09553-0.
  11. David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. Abella: A system for reasoning about relational specifications. Journal of Formalized Reasoning, 7(2):1-89, 2014. URL: https://doi.org/10.6092/issn.1972-5787/4650.
  12. Jesper Bengtson and Joachim Parrow. Formalising the pi-calculus using nominal logic. Log. Methods Comput. Sci., 5(2), 2009. URL: http://arxiv.org/abs/0809.3960.
  13. Malgorzata 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. URL: https://doi.org/10.1109/LICS.2017.8005118.
  14. Gérard Boudol. The p-calculus in direct style. High. Order Symb. Comput., 11(2):177-208, 1998. URL: https://doi.org/10.1023/A:1010064516533.
  15. Gérard Boudol and Cosimo Laneve. The discriminating power of multiplicities in the lambda-calculus. Inf. Comput., 126(1):83-102, 1996. URL: https://doi.org/10.1006/inco.1996.0037.
  16. Xiaojuan Cai and Yuxi Fu. The λ-calculus in the π-calculus. Math. Struct. Comput. Sci., 21(5):943-996, 2011. URL: https://doi.org/10.1017/S0960129511000260.
  17. Kaustuv Chaudhuri, Matteo Cimini, and Dale Miller. A lightweight formalization of the metatheory of bisimulation-up-to. In Xavier Leroy and Alwen Tiu, editors, Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs, pages 157-166, Mumbai, India, January 2015. ACM. URL: https://doi.org/10.1145/2676724.2693170.
  18. Matteo Cimini, Claudio Sacerdoti Coen, and Davide Sangiorgi. Functions as processes: Termination and the λμμ̃-calculus. In Martin Wirsing, Martin Hofmann, and Axel Rauschmayer, editors, Trustworthly Global Computing - 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers, volume 6084 of Lecture Notes in Computer Science, pages 73-86. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15640-3_5.
  19. Joëlle Despeyroux. A higher-order specification of the pi-calculus. In Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics, International Conference IFIP TCS 2000, Sendai, Japan, August 17-19, 2000, Proceedings, volume 1872 of Lecture Notes in Computer Science, pages 425-439. Springer, 2000. URL: https://doi.org/10.1007/3-540-44929-9_30.
  20. Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi. Eager functions as processes. Theor. Comput. Sci., 913:8-42, 2022. URL: https://doi.org/10.1016/j.tcs.2022.01.043.
  21. Murdoch J. Gabbay. The π-Calculus in FM, pages 247-269. Springer Netherlands, Dordrecht, 2003. URL: https://doi.org/10.1007/978-94-017-0253-9_10.
  22. Andrew Gacek. The abella interactive theorem prover (system description). In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science, pages 154-161. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71070-7_13.
  23. Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Inf. Comput., 209(1):48-73, 2011. URL: https://doi.org/10.1016/j.ic.2010.09.004.
  24. Simon J. Gay. A framework for the formalisation of pi calculus type systems in isabelle/hol. In Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, volume 2152 of Lecture Notes in Computer Science, pages 217-232. Springer, 2001. URL: https://doi.org/10.1007/3-540-44755-5_16.
  25. Daniel Hirschkoff. A full formalisation of pi-calculus theory in the calculus of constructions. In Elsa L. Gunter and Amy P. Felty, editors, Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, volume 1275 of Lecture Notes in Computer Science, pages 153-169. Springer, 1997. URL: https://doi.org/10.1007/BFb0028392.
  26. Furio Honsell, Marino Miculan, and Ivan Scagnetto. π-calculus in (co)inductive type theories. Theoretical Computer Science, 2(253):239-285, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00095-5.
  27. Guilhem Jaber and Davide Sangiorgi. Games, mobile processes, and functions. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 25:1-25:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.25.
  28. Naoki Kobayashi. A partially deadlock-free typed process calculus. ACM Trans. Program. Lang. Syst., 20(2):436-482, 1998. URL: https://doi.org/10.1145/276393.278524.
  29. Thomas F. Melham. A mechanized theory of the pi-calculus in HOL. Nord. J. Comput., 1(1):50-76, 1994. Google Scholar
  30. Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, 2012. URL: http://www.cambridge.org/de/academic/subjects/computer-science/programming-languages-and-applied-logic/programming-higher-order-logic?format=HB.
  31. Dale Miller and Alwen Tiu. A proof theory for generic judgments. ACM Trans. Comput. Log., 6(4):749-783, 2005. URL: https://doi.org/10.1145/1094622.1094628.
  32. Robin Milner. Functions as processes. Math. Struct. Comput. Sci., 2(2):119-141, 1992. URL: https://doi.org/10.1017/S0960129500001407.
  33. Robin Milner. Local bigraphs and confluence: Two conjectures: (extended abstract). In Roberto M. Amadio and Iain Phillips, editors, Proceedings of the 13th International Workshop on Expressiveness in Concurrency, EXPRESS 2006, Bonn, Germany, August 26, 2006, volume 175 of Electronic Notes in Theoretical Computer Science, pages 65-73. Elsevier, 2006. URL: https://doi.org/10.1016/j.entcs.2006.07.035.
  34. Otmane Aït Mohamed. Mechanizing a pi-calculus equivalence in HOL. In Higher Order Logic Theorem Proving and Its Applications, 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995, Proceedings, volume 971 of Lecture Notes in Computer Science, pages 1-16. Springer, 1995. URL: https://doi.org/10.1007/3-540-60275-5_53.
  35. Joachim Niehren. Functional computation as concurrent computation. In Hans-Juergen Boehm and Guy L. Steele Jr., editors, Conference Record of POPL'96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996, pages 333-343. ACM Press, 1996. URL: https://doi.org/10.1145/237721.237801.
  36. Dominic A. Orchard and Nobuko Yoshida. Using session types as an effect system. In Proceedings Eighth International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES 2015, London, UK, 18th April 2015, volume 203 of EPTCS, pages 1-13, 2015. URL: https://doi.org/10.4204/EPTCS.203.1.
  37. Roly Perera and James Cheney. Proof-relevant π-calculus: a constructive account of concurrency and causality. Math. Struct. Comput. Sci., 28(9):1541-1577, 2018. URL: https://doi.org/10.1017/S096012951700010X.
  38. Christine Röckl, Daniel Hirschkoff, and Stefan Berghofer. Higher-order abstract syntax with induction in isabelle/hol: Formalizing the pi-calculus and mechanizing the theory of contexts. In Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings, volume 2030 of Lecture Notes in Computer Science, pages 364-378. Springer, 2001. URL: https://doi.org/10.1007/3-540-45315-6_24.
  39. Davide Sangiorgi. The lazy lambda calculus in a concurrency scenario. Inf. Comput., 111(1):120-153, 1994. URL: https://doi.org/10.1006/inco.1994.1042.
  40. Davide Sangiorgi. From lambda to pi; or, rediscovering continuations. Math. Struct. Comput. Sci., 9(4):367-401, 1999. URL: http://journals.cambridge.org/action/displayAbstract?aid=44843.
  41. Davide Sangiorgi and David Walker. The Pi-Calculus - a theory of mobile processes. Cambridge University Press, 2001. Google Scholar
  42. Davide Sangiorgi and Xian Xu. Trees from functions as processes. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:11)2018.
  43. Alwen Tiu and Dale Miller. Proof search specifications of bisimulation and modal logics for the pi-calculus. ACM Trans. Comput. Log., 11(2):13:1-13:35, 2010. URL: https://doi.org/10.1145/1656242.1656248.
  44. Bernardo Toninho, Luís Caires, and Frank Pfenning. Functions as session-typed processes. In Lars Birkedal, editor, Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7213 of Lecture Notes in Computer Science, pages 346-360. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28729-9_23.
  45. Niccolò Veltri and Andrea Vezzosi. Formalizing π-calculus in guarded cubical agda. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 270-283. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373814.
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