Abstract
For many application-level distributed protocols and parallel algorithms, the set of participants, the number of messages or the interaction structure are only known at run-time. This paper proposes a dependent type theory for multiparty sessions which can statically guarantee type-safe, deadlock-free multiparty interactions among processes whose specifications are parameterised by indices. We use the primitive recursion operator from Gödel’s System \(\mathcal T\) to express a wide range of communication patterns while keeping type checking decidable. We illustrate our type theory through non-trivial programming and verification examples taken from parallel algorithms and Web services usecases.
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.
The work is partially supported by EPSRC EP/G015635/1 and EP/F003757/1.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Aspinall, D., Hofmann, M.: Dependent Types. In: Advanced Topics in Types and Programming Languages. MIT Press, Cambridge (2005)
Ateniese, G., Steiner, M., Tsudik, G.: Authenticated group key agreement and friends. In: CCS 1998: Proceedings of the 5th ACM conference on Computer and communications security, pp. 17–26. ACM, New York (1998)
Bettini, L., et al.: Global progress in dynamically interfered multiparty sessions. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 418–433. Springer, Heidelberg (2008)
Bhargavan, K., Corin, R., Deniélou, P.-M., Fournet, C., Leifer, J.: Cryptographic protocol synthesis and verification for multiparty sessions. In: CSF, pp. 124–140 (2009)
Bonelli, E., Compagnoni, A.: Multipoint session types for a distributed calculus. In: Barthe, G., Fournet, C. (eds.) TGC 2007 and FODO 2008. LNCS, vol. 4912, pp. 240–256. Springer, Heidelberg (2008)
Caires, L., Vieira, H.T.: Conversation types. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 285–300. Springer, Heidelberg (2009)
Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred programming for web services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 2–17. Springer, Heidelberg (2007)
Carbone, M., Yoshida, N., Honda, K.: Asynchronous session types: Exceptions and multiparty interactions. In: Bernardo, M., Padovani, L., Zavattaro, G. (eds.) SFM 2009. LNCS, vol. 5569, pp. 187–212. Springer, Heidelberg (2009)
Castagna, G., Padovani, L.: Contracts for mobile processes. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009 - Concurrency Theory. LNCS, vol. 5710, pp. 211–228. Springer, Heidelberg (2009)
Cooley, J.W., Tukey, J.W.: An algorithm for the machine calculation of complex fourier series. Mathematics of Computation 19(90), 297–301 (1965)
Online Appendix, http://www.doc.ic.ac.uk/~yoshida/dependent/
Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. CUP, Cambridge (1989)
Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchronous Session Types. In: POPL 2008, pp. 273–284. ACM, New York (2008)
Hu, R., Yoshida, N., Honda, K.: Session-Based Distributed Programming in Java. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 516–541. Springer, Heidelberg (2008)
Leighton, F.T.: Introduction to parallel algorithms and architectures: arrays, trees, hypercubes. Morgan Kaufmann, San Francisco (1991)
Martin-Lőf, P.: Infinite terms and a system of natural deduction. In: Compositio Mathematica, pp. 93–103. Wolters-Noordhoof (1972)
Mostrous, D., Yoshida, N., Honda, K.: Global principal typing in partially commutative asynchronous sessions. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 316–332. Springer, Heidelberg (2009)
Nelson, N.: Primitive recursive functionals with dependent types. In: Schmidt, D., Main, M.G., Melton, A.C., Mislove, M.W., Brookes, S.D. (eds.) MFPS 1991. LNCS, vol. 598, pp. 125–143. Springer, Heidelberg (1992)
Web Services Choreography Requirements (No. 11), http://www.w3.org/TR/ws-chor-reqs
Tait, W.W.: Infinitely long terms of transfinite type. In: Formal Systems and Recursive Functions, pp. 177–185. North Holland, Amsterdam (1965)
Web Services Choreography Working Group. Choreography Description Language, http://www.w3.org/2002/ws/chor/
Xi, H., Pfenning, F.: Dependent types in practical programming. In: POPL, pp. 214–227 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yoshida, N., Deniélou, PM., Bejleri, A., Hu, R. (2010). Parameterised Multiparty Session Types . In: Ong, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2010. Lecture Notes in Computer Science, vol 6014. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12032-9_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-12032-9_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12031-2
Online ISBN: 978-3-642-12032-9
eBook Packages: Computer ScienceComputer Science (R0)