Abstract
We extend the linear π-calculus with composite and equi-recursive types in a way that enables the sharing of data containing linear values, provided that there is no overlapping access on such values. We show that the extended type system admits a complete type reconstruction algorithm and, as a by-product, we solve the problem of reconstruction for equi-recursive session types.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Courcelle, B.: Fundamental properties of infinite trees. Theor. Comp. Sci. 25, 95–169 (1983)
Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. In: PPDP 2012, pp. 139–150. ACM (2012)
Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993)
Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)
Igarashi, A.: Type-based analysis of usage of values for concurrent programming languages (1997), http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/papers/
Igarashi, A., Kobayashi, N.: Type-based analysis of communication for concurrent programming languages. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol. 1302, pp. 187–201. Springer, Heidelberg (1997)
Igarashi, A., Kobayashi, N.: Type Reconstruction for Linear π-Calculus with I/O Subtyping. Inf. and Comp. 161(1), 1–44 (2000)
Kobayashi, N.: Quasi-linear types. In: POPL 1999, pp. 29–42. ACM (1999)
Kobayashi, N.: Type systems for concurrent programs. In: Aichernig, B.K. (ed.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 439–453. Springer, Heidelberg (2003), Extended version at http://www.kb.ecei.tohoku.ac.jp/~koba/papers/tutorial-type-extended.pdf
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)
Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. 21(5), 914–947 (1999)
Mezzina, L.G.: How to infer finite session types in a calculus of services and sessions. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 216–231. Springer, Heidelberg (2008)
Nestmann, U., Steffen, M.: Typing confluence. In: FMICS 1997, pp. 77–101 (1997), Also available as report ERCIM-10/97-R052, European Research Consortium for Informatics and Mathematics (1997)
Sangiorgi, D., Walker, D.: The Pi-Calculus - A theory of mobile processes. Cambridge University Press (2001)
Turner, D.N., Wadler, P., Mossin, C.: Once upon a type. In: FPCA 1995, pp. 1–11 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Padovani, L. (2014). Type Reconstruction for the Linear π-Calculus with Composite and Equi-Recursive Types. In: Muscholl, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2014. Lecture Notes in Computer Science, vol 8412. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54830-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-54830-7_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54829-1
Online ISBN: 978-3-642-54830-7
eBook Packages: Computer ScienceComputer Science (R0)