Intersection types and runtime errors in the pi-calculus

Abstract

We introduce a type system for the π-calculus which is designed to guarantee that typable processes are well-behaved, namely they never produce a run-time error and, even if they may diverge, there is always a chance for them to “finish their work”, i.e., to reduce to an idle process. The introduced type system is based on non-idempotent intersections, and is thus very powerful as for the class of processes it can capture. Indeed, despite the fact that the underlying property is Π₂⁰-complete, there is a way to show that the system is complete, i.e., that any well-behaved process is typable, although for obvious reasons infinitely many derivations need to be considered.

References

1. Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. 2018. Tight typings and split bounds. PACMPL 2, ICFP (2018), 94:1–94:30.
2. J. W. Backus, F. L. Bauer, J. Green, C. Katz, J. McCarthy, P. Naur, A. J. Perlis, H. Rutishauser, K. Samelson, B. Vauquois, J. H. Wegstein, A. van Wijngaarden, M. Woodger, and W. L. van der Poel. 1962. Revised report on the algorithmic languageAlgol 60. Numer. Math. 1 (1962), 420–453.
3. Henk P. Barendregt. 1984. The Lambda Calculus (revised ed.). North Holland.
4. Flavien Breuvart and Ugo Dal Lago. 2018. On Intersection Types and Probabilistic Lambda Calculi. In Proc. of PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, David Sabel and Peter Thiemann (Eds.). ACM, 8:1–8:13.
5. Luís Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions, See { Gastin and Laroussinie 2010 }, 222–236.
6. Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, and Daniele Varacca. 2006. Encoding CDuce in the Cpi-Calculus. In Proc. of CONCUR 2006. 310–326.
7. Mario Coppo and Mariangiola Dezani-Ciancaglini. 1978. A new type assignment for λ-terms. Arch. Math. Log. 19, 1 (1978), 139–156.
8. Mario Coppo and Mariangiola Dezani-Ciancaglini. 1980. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic 21, 4 (1980), 685–693.
9. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1981. Functional Characters of Solvable Terms. Math. Log. Q. 27, 2-6 (1981), 45–58.
10. Ugo Dal Lago and Marco Gaboardi. 2011. Linear Dependent Types and Relative Completeness. Logical Methods in Computer Science 8, 4 (2011).
11. Ugo Dal Lago, Ryo Tanaka, and Akira Yoshimizu. 2017. The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens. In Proc. of LICS 2017, Reykjavik, Iceland, June 20-23, 2017. IEEE Computer Society, 1–12.
12. Daniel de Carvalho. 2018. Execution time of λ-terms via denotational semantics and intersection types. Mathematical Structures in Computer Science 28, 7 (2018), 1169–1203.
13. Marc de Visme and Damiano Mazza. 2017. On the Concurrent Meaning of Logical Correctness. (2017). Unpublished manuscript. Available on the second author’s web page.
14. Romain Demangeon, Daniel Hirschkoff, and Davide Sangiorgi. 2010a. Termination in higher-order concurrent calculi. J. Log. Algebr. Program. 79, 7 (2010), 550–577.
15. Romain Demangeon, Daniel Hirschkoff, and Davide Sangiorgi. 2010b. Termination in Impure Concurrent Languages, See { Gastin and Laroussinie 2010 }, 328–342.
16. Yuxin Deng and Davide Sangiorgi. 2004. Towards an Algebraic Theory of Typed Mobile Processes. In Proc. of ICALP 2004, Turku, Finland, July 12-16, 2004. 445–456.
17. Thomas Ehrhard and Olivier Laurent. 2010. Interpreting a Finitary Pi-Calculus in Differential Interaction Nets. Information and Computation 208, 6 (2010), 606–633.
18. Timothy S. Freeman and Frank Pfenning. 1991. Refinement Types for ML. In Proc. of PLDI, Toronto, Ontario, Canada, June 26-28, 1991. 268–277.
19. Paul Gastin and François Laroussinie (Eds.). 2010. CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings. Lecture Notes in Computer Science, Vol. 6269. Springer.
20. Jean-Yves Girard. 1971. Une extension de l’interpretation de Gödel a l’analyse, et son application a l’élimination des coupures dans l’analyse et la théorie des types. In Proc. of the Second Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics, Vol. 63. Elsevier, 63 – 92.
21. Jean-Yves Girard. 1987. Linear Logic. Theor. Comput. Sci. 50, 1 (1987), 1–102.
22. Jean-Yves Girard. 1989. Geometry of Interaction I: interpretation of System F. In Proc. of the Logic Colloquium ’88. North Holland, 221–260.
23. Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. 1992. Bounded linear logic: a modular approach to polynomial-time. Theoretical Computer Science 97, 1 (1992), 1–66.
24. Kohei Honda and Olivier Laurent. 2010. An exact correspondence between a typed pi-calculus and polarised proof-nets. Theor. Comput. Sci 411, 22-24 (2010), 2223–2238.
25. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In Proc. of ESOP. 122–138.
26. Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty asynchronous session types. In Proc. of POPL 2008, San Francisco, California, USA, January 7-12, 2008. 273–284.
27. John Hughes, Lars Pareto, and Amr Sabry. 1996. Proving the Correctness of Reactive Systems Using Sized Types. In Proc. of POPL 1996. 410–423.
28. Paris C. Kanellakis, Gerd G. Hillebrand, and Harry G. Mairson. 1994. An Analysis of the Core-ML Language: Expressive Power and Type Reconstruction. In Proc. of ICALP 1994 (Lecture Notes in Computer Science), Vol. 820. Springer, 83–105.
29. Naoki Kobayashi. 2000. Type Systems for Concurrent Processes: From Deadlock-Freedom to Livelock-Freedom, TimeBoundedness. In Proc. of IFIP TCS 2000, Sendai, Japan, August 17-19, 2000. 365–389.
30. Naoki Kobayashi. 2006. A New Type System for Deadlock-Free Processes. In Proc. of CONCUR 2006. 233–247.
31. Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. 1999. Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. 21, 5 (1999), 914–947.
32. Jean-Louis Krivine. 1993. Lambda-calculus, types and models. Masson.
33. Damiano Mazza, Luc Pellissier, and Pierre Vial. 2018. Polyadic approximations, fibrations and intersection types. PACMPL 2, POPL (2018), 6:1–6:28.
34. Robin Milner. 1978. A theory of type polymorphism in programming. J. Comput. System Sci. 17, 3 (1978), 348 – 375.
35. Robin Milner. 1992. Functions as Processes. Mathematical Structures in Computer Science 2, 2 (1992), 119–141.
36. Luca Padovani. 2014. Deadlock and lock freedom in the linear π -calculus. In Proc. of CSL-LICS ’14, Vienna, Austria, July 14 -18, 2014. 72:1–72:10.
37. Mauro Piccolo. 2012. Strong Normalization in the π -calculus with Intersection and Union Types. Fundam. Inform. 121, 1-4 (2012), 227–252.
38. John C. Reynolds. 1974. Towards a Theory of Type Structure. In Proc. of Programming Symposium, Colloque Sur La Programmation. Springer-Verlag, 408–423.
39. Davide Sangiorgi and David Walker. 2001. The Pi-Calculus - a theory of mobile processes. Cambridge University Press.
40. Alex K. Simpson. 2005. Reduction in a Linear Lambda-Calculus with Applications to Operational Semantics. In Proc. of RTA 2005, Nara, Japan, April 19-21, 2005 (Lecture Notes in Computer Science), Jürgen Giesl (Ed.), Vol. 3467. Springer, 219–234.
41. Kohei Suenaga and Naoki Kobayashi. 2007. Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts. In Proc. of ESOP 2007. 490–504.
42. Philip Wadler. 2014. Propositions as sessions. J. Funct. Program. 24, 2-3 (2014), 384–418.
43. J. B. Wells. 1994. Typability and Type-Checking in the Second-Order lambda-Calculus are Equivalent and Undecidable. In Proc. of LICS 1994. IEEE Computer Society, 176–185.
44. Nobuko Yoshida, Martin Berger, and Kohei Honda. 2004. Strong normalisation in the pi-calculus. Information and Computation 191, 2 (2004), 145–202.

Index Terms

• Theory of computation

  • Logic

    • Linear logic

  • Models of computation

    • Concurrency

      • Process calculi

  • Semantics and reasoning

    • Program constructs

      • Type structures