Document Open Access Logo

Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes

Authors Joseph W. N. Paulus , Daniele Nantes-Sobrinho , Jorge A. Pérez

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2021.11.pdf
  • Filesize: 0.98 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
  • Theory of computation → Process calculi
Keywords
  • Resource λ-calculus
  • intersection types
  • session types
  • process calculi

Metrics

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

Abstract

Type-preserving translations are effective rigorous tools in the study of core programming calculi. In this paper, we develop a new typed translation that connects sequential and concurrent calculi; it is governed by type systems that control resource consumption. Our main contribution is the source language, a new resource λ-calculus with non-collapsing non-determinism and failures, dubbed uλ^{↯}_{⊕}. In uλ^{↯}_{⊕}, resources are split into linear and unrestricted; failures are explicit and arise from this distinction. We define a type system based on intersection types to control resources and fail-prone computation. The target language is 𝗌π, an existing session-typed π-calculus that results from a Curry-Howard correspondence between linear logic and session types. Our typed translation subsumes our prior work; interestingly, it treats unrestricted resources in uλ^{↯}_{⊕} as client-server session behaviours in 𝗌π.

Cite As Get BibTex

Joseph W. N. Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez. Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 11:1-11:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.TYPES.2021.11

Author Details

Joseph W. N. Paulus
  • University of Groningen, The Netherlands
Daniele Nantes-Sobrinho
  • University of Brasília, Brazil
  • Imperial College London, UK
Jorge A. Pérez
  • University of Groningen, The Netherlands

Funding

Research partially supported by the Dutch Research Council (NWO) under project No. 016.Vidi.189.046 (Unifying Correctness for Communicating Software).

Acknowledgements

We are grateful to the anonymous reviewers for their constructive feedback.

References

  1. Gérard Boudol. The lambda-calculus with multiplicities (abstract). In Eike Best, editor, CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, volume 715 of Lecture Notes in Computer Science, pages 1-6. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_1.
  2. 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.
  3. Gérard Boudol and Cosimo Laneve. lambda-calculus, multiplicities, and the pi-calculus. In Proof, Language, and Interaction, Essays in Honour of Robin Milner, pages 659-690, 2000. Google Scholar
  4. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL, 25(4):431-464, 2017. Google Scholar
  5. Luís Caires and Jorge A. Pérez. Linearity, control effects, and behavioral types. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 of Lecture Notes in Computer Science, pages 229-259. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_9.
  6. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, pages 222-236, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_16.
  7. Maurizio Dominici, Simona Ronchi Della Rocca, and Paolo Tranquilli. Standardization in resource lambda-calculus. In Proceedings 2nd International Workshop on Linearity, LINEARITY 2012, Tallinn, Estonia, 1 April 2012., pages 1-11, 2012. URL: https://doi.org/10.4204/EPTCS.101.1.
  8. Silvia Ghilezan, Jelena Ivetic, Pierre Lescanne, and Silvia Likavec. Intersection types for the resource control lambda calculi. In Theoretical Aspects of Computing - ICTAC 2011 - 8th International Colloquium, Johannesburg, South Africa, August 31 - September 2, 2011. Proceedings, pages 116-134, 2011. URL: https://doi.org/10.1007/978-3-642-23283-1_10.
  9. Daniele Gorla. Towards a unified approach to encodability and separation results for process calculi. Inf. Comput., 208(9):1031-1053, 2010. URL: https://doi.org/10.1016/j.ic.2010.05.002.
  10. 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, 2013. URL: https://doi.org/10.1109/LICS.2013.37.
  11. Kohei Honda. Types for dyadic interaction. In Eike Best, editor, CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, volume 715 of Lecture Notes in Computer Science, pages 509-523. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
  12. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, Programming Languages and Systems - ESOP'98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. URL: https://doi.org/10.1007/BFb0053567.
  13. Delia Kesner and Stéphane Lengrand. Resource operators for lambda-calculus. Inf. Comput., 205(4):419-473, 2007. URL: https://doi.org/10.1016/j.ic.2006.08.008.
  14. Dimitrios Kouzapas, Jorge A. Pérez, and Nobuko Yoshida. On the relative expressiveness of higher-order session processes. Inf. Comput., 268, 2019. URL: https://doi.org/10.1016/j.ic.2019.06.002.
  15. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I. Inf. Comput., 100(1):1-40, 1992. URL: https://doi.org/10.1016/0890-5401(92)90008-4.
  16. Michele Pagani and Simona Ronchi Della Rocca. Solvability in resource lambda-calculus. In C.-H. Luke Ong, editor, Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6014 of Lecture Notes in Computer Science, pages 358-373. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12032-9_25.
  17. Joseph W. N. Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez. Non-deterministic functions as non-deterministic processes. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 21:1-21:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.21.
  18. Joseph W. N. Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez. Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes (Extended Version). CoRR, abs/2112.01593, 2021. URL: http://arxiv.org/abs/2112.01593.
  19. Philip Wadler. Propositions as sessions. In Peter Thiemann and Robby Bruce Findler, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012, pages 273-286. ACM, 2012. URL: https://doi.org/10.1145/2364527.2364568.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact