Types for Deadlock-Free Higher-Order Programs

  • Luca PadovaniEmail author
  • Luca Novara
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9039)


Type systems for communicating processes are typically studied using abstract models – e.g., process algebras – that distill the communication behavior of programs but overlook their structure in terms of functions, methods, objects, modules. It is not always obvious how to apply these type systems to structured programming languages. In this work we port a recently developed type system that ensures deadlock freedom in the π-calculus to a higher-order language.


Type System Parallel Composition Side Condition Typing Rule Level Polymorphism 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Amtoft, T., Nielson, F., Nielson, H.: Type and Effect Systems: Behaviours for Concurrency. Imperial College Press (1999)Google Scholar
  2. 2.
    Bono, V., Padovani, L., Tosatto, A.: Polymorphic Types for Leak Detection in a Session-Oriented Functional Language. In: Beyer, D., Boreale, M. (eds.) FMOODS/FORTE 2013. LNCS, vol. 7892, pp. 83–98. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  3. 3.
    Carbone, M., Dardha, O., Montesi, F.: Progress as compositional lock-freedom. In: Kühn, E., Pugliese, R. (eds.) COORDINATION 2014. LNCS, vol. 8459, pp. 49–64. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  4. 4.
    Courcelle, B.: Fundamental properties of infinite trees. Theor. Comp. Sci. 25, 95–169 (1983)CrossRefzbMATHMathSciNetGoogle Scholar
  5. 5.
    Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. In: PPDP 2012, pp. 139–150. ACM (2012)Google Scholar
  6. 6.
    Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19–50 (2010)CrossRefzbMATHMathSciNetGoogle Scholar
  7. 7.
    Kobayashi, N.: A type system for lock-free processes. Inf. and Comp. 177(2), 122–159 (2002)CrossRefzbMATHGoogle Scholar
  8. 8.
    Kobayashi, N.: A new type system for deadlock-free processes. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 233–247. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  9. 9.
    Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. 21(5), 914–947 (1999)CrossRefGoogle Scholar
  10. 10.
    Padovani, L.: Deadlock and Lock Freedom in the Linear π-Calculus. In: CSL-LICS 2014, pp. 72:1–72:10. ACM (2014),
  11. 11.
    Padovani, L.: Type Reconstruction for the Linear π-Calculus with Composite and Equi-Recursive Types. In: Muscholl, A. (ed.) FOSSACS 2014. LNCS, vol. 8412, pp. 88–102. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  12. 12.
    Padovani, L., Chen, T.-C., Tosatto, A.: Type Reconstruction Algorithms for Deadlock-Free and Lock-Free Linear π-Calculi. In: Holvoet, T., Viroli, M. (eds.) COORDINATION 2015. LNCS, vol. 9037, pp. 85–100. Springer, Heidelberg (2015)CrossRefGoogle Scholar
  13. 13.
    Padovani, L., Novara, L.: Types for Deadlock-Free Higher-Order Concurrent Programs. Technical report, Università di Torino (2014),
  14. 14.
    Wadler, P.: Propositions as sessions. In: ICFP 2012, pp. 273–286. ACM (2012)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2015

Authors and Affiliations

  1. 1.Dipartimento di InformaticaUniversità di TorinoTorinoItaly

Personalised recommendations